CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIn 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.
| Titolo: | An application of automated equational reasoning to many-valued logic |
| Autori: | |
| Data di pubblicazione: | 1991 |
| Serie: | |
| Handle: | http://hdl.handle.net/11562/16060 |
| ISBN: | 9783540543176 |
| Appare nelle tipologie: | 02.01 Contributo in volume (Capitolo o Saggio) |
File in questo prodotto:
Copyright © 2020