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.
KBlab: an equational theorem prover for the Macintosh
BONACINA, Maria Paola
;
1989-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
RTA1989KBlab.pdf
accesso aperto
Descrizione: Articolo
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
136.07 kB
Formato
Adobe PDF
|
136.07 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.