KBlab: an equational theorem prover for the Macintosh

This paper describes KBlab, a Macintosh theorem prover for equational logic. KBlab is a user friendly, portable, low cost theorem prover, which requires only nominal resources to run. The core of KBlab is the Knuth-Bendix Completion Procedure, extended to Unfailing Knuth-Bendix, S-strategy and inductive theorem proving. Its new features include a choice of eight different search strategies for axiom selection and the ability for the user to change the search strategy during a Completion run. Experimental results show that the choice of the strategy employed has a great impact on termination and number of equations generated. Some of these results are listed in the paper. KBlab provides the user with a complete environment for running proof sessions. It is possible to edit theories, execute the Completion procedures, store the proof traces and even modify the search strategy, all within the same environment. We believe that these unique features make it a convenient tool for experimenting in automated reasoning.