Unification in Intuitionistic Logic
Ghilardi, Silvio
J. Symbolic Logic, Tome 64 (1999) no. 1, p. 859-880 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.
Publié le : 1999-06-14
Classification:  E-Unification,  Projective Heyting Algebras,  Exact Formulas,  Admissible Inference Rules,  03B20,  68T15,  03B55,  06D20,  08B30 
@article{1183745815,
     author = {Ghilardi, Silvio},
     title = {Unification in Intuitionistic Logic},
     journal = {J. Symbolic Logic},
     volume = {64},
     number = {1},
     year = {1999},
     pages = { 859-880},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183745815}
}

Ghilardi, Silvio. Unification in Intuitionistic Logic. J. Symbolic Logic, Tome 64 (1999) no. 1, pp.  859-880. http://gdmltest.u-ga.fr/item/1183745815/