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.
1989
9783540510819
Knuth-Bendix completion, equational theorem proving
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16062
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact