In this paper we present the theorem prover SBR3 for equational logic and itsapplication in the many-valued logic of Lukasiewicz. We give a new equational axiomatization of many-valued logic and we prove by SBR3 that it is equivalent to the classical equational presentation of such logic given by Wajsberg. We feel that our equational axiomatization of Wajsberg algebras is better suited for automated reasoning than the classical one. Indeed, it has allowed us to obtain a fast mechanical proof of the so called "fifth Lukasiewicz conjecture'', which is regarded as a challenge problem for theorem provers.

An application of automated equational reasoning to many-valued logic

BONACINA, Maria Paola
1991-01-01

Abstract

In this paper we present the theorem prover SBR3 for equational logic and itsapplication in the many-valued logic of Lukasiewicz. We give a new equational axiomatization of many-valued logic and we prove by SBR3 that it is equivalent to the classical equational presentation of such logic given by Wajsberg. We feel that our equational axiomatization of Wajsberg algebras is better suited for automated reasoning than the classical one. Indeed, it has allowed us to obtain a fast mechanical proof of the so called "fifth Lukasiewicz conjecture'', which is regarded as a challenge problem for theorem provers.
1991
9783540543176
Automated theorem proving; many-valued logic; contraction-based theorem proving
File in questo prodotto:
File Dimensione Formato  
CTRS1990sbr3.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 225.34 kB
Formato Adobe PDF
225.34 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/16060
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 0
social impact