We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.

Factor Varieties and Symbolic Computation

SALIBRA, Antonino;FAVRO, GIORDANO;MANZONETTO, Giulio
2016-01-01

Abstract

We propose an algebraization of classical and non-classical logics, based on factor varieties and decomposition operators. In particular, we provide a new method for determining whether a propositional formula is a tautology or a contradiction. This method can be automatized by defining a term rewriting system that enjoys confluence and strong normalization. This also suggests an original notion of logical gate and circuit, where propositional variables becomes logical gates and logical operations are implemented by substitution. Concerning formulas with quantifiers, we present a simple algorithm based on factor varieties for reducing first-order classical logic to equational logic. We achieve a completeness result for first-order classical logic without requiring any additional structure.
2016
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)
File in questo prodotto:
File Dimensione Formato  
lics16 copy.pdf

accesso aperto

Descrizione: pdf
Tipologia: Documento in Pre-print
Licenza: Accesso gratuito (solo visione)
Dimensione 390.74 kB
Formato Adobe PDF
390.74 kB Adobe PDF Visualizza/Apri
2933575.2933600.pdf

non disponibili

Tipologia: Versione dell'editore
Licenza: Accesso chiuso-personale
Dimensione 385.55 kB
Formato Adobe PDF
385.55 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA 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/10278/3679739
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact