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

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.
9783540543176
Automated theorem proving; many-valued logic; contraction-based theorem proving
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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