×

Unification, finite duality and projectivity in varieties of Heyting algebras. (English) Zbl 1058.03020

Addressed mainly to logicians, this article may also be of interest for computer scientists. Unification with respect to an equational theory was algebrized by the author [J. Log. Comput. 7, No. 6, 733–752 (1997; Zbl 0894.08004)] so as to utilize categorical duality theory for the determination of unification types in locally finite varieties of Heyting algebras, which is illustrated in the present paper. Although the unification algorithms that can indeed be extracted from this setting might be inefficient, the constructively found unification types may give a hint at a chance to improve the algorithms.

MSC:

03B35 Mechanization of proofs and logical operations
06D20 Heyting algebras (lattice-theoretic aspects)
08B30 Injectives, projectives
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 0894.08004
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Albert, M. H., Category equivalence preserves unification type, Algebra Universalis, 36, 457-466 (1996) · Zbl 0902.08014
[2] F. Baader, Characterizations of Unification Type Zero, Proc. RTA ’89, Lecture Notes in Computer Science, vol. 355, Springer, Berlin, 1989, pp. 2-14.; F. Baader, Characterizations of Unification Type Zero, Proc. RTA ’89, Lecture Notes in Computer Science, vol. 355, Springer, Berlin, 1989, pp. 2-14.
[3] F. Baader, W. Snyder, Unification theory, in: A. Voronkov, A. Robinson (Eds.), Handbook of Automated Reasoning, vol. I, Elsevier, Amsterdam, MIT Press, Cambridge, MA, 2001, pp. 445-533.; F. Baader, W. Snyder, Unification theory, in: A. Voronkov, A. Robinson (Eds.), Handbook of Automated Reasoning, vol. I, Elsevier, Amsterdam, MIT Press, Cambridge, MA, 2001, pp. 445-533. · Zbl 1011.68126
[4] Bellissima, F., Finitely generated free Heyting algebras, J. Symbolic Logic, 51, 152-165 (1986) · Zbl 0616.03021
[5] F. Borceux, Handbook of Categorical Algebra, vol. II, Cambridge University Press, Cambridge, 1994.; F. Borceux, Handbook of Categorical Algebra, vol. II, Cambridge University Press, Cambridge, 1994. · Zbl 0911.18001
[6] Chagrov, A.; Zakharyaschev, M., Model Logic (1997), Oxford University Press: Oxford University Press Oxford
[7] S. Ghilardi, Irreducible models and definable embeddings, in: Logic Colloquium 92, Proc., CSLI Publications, Stanford, CA, 1995, pp. 95-213.; S. Ghilardi, Irreducible models and definable embeddings, in: Logic Colloquium 92, Proc., CSLI Publications, Stanford, CA, 1995, pp. 95-213.
[8] Ghilardi, S., Unification through projectivity, J. Logic Comput., 7, 6, 733-752 (1997) · Zbl 0894.08004
[9] Ghilardi, S., Unification in intuitionistic logic, J. Symbolic Logic, 64, 2, 859-880 (1999) · Zbl 0930.03009
[10] Ghilardi, S., Best solving modal equations, Ann. Pure Appl. Logic, 102, 183-198 (2000) · Zbl 0949.03010
[11] Ghilardi, S., A resolution/tableaux algorithm for projective approximations in IPC, Logic J. of the IGPL, 10, 3, 227-241 (2002) · Zbl 1005.03504
[12] S. Ghilardi, L. Sacchetti, Filtering Unification and Most General Unifiers in Modal Logic, preprint, 2003.; S. Ghilardi, L. Sacchetti, Filtering Unification and Most General Unifiers in Modal Logic, preprint, 2003. · Zbl 1069.03011
[13] Ghilardi, S.; Zawadowski, M., Sheaves, Games and Model Completions, Trends in Logic Series (2002), Kluwer: Kluwer Dordrecht · Zbl 1036.03001
[14] Martin, U.; Nipkow, T., Boolean Unification—the story so far, J. Symbolic Comput., 7, 275-293 (1989) · Zbl 0682.68093
[15] Nipkow, T., Unification in primal algebras, their powers and their varieties, J. Assoc. Comput. Mach., 37, 742-776 (1990) · Zbl 0711.68092
[16] Quackenbush, R. W., Demi-semi-primal algebras and Mal’cev-type conditions, Math. Z., 122, 166-176 (1971) · Zbl 0209.04302
[17] Rybakov, V. V., Rules of inference with parameters for intuitionistic logic, J. Symbolic Logic, 57, 3, 912-923 (1992) · Zbl 0788.03007
[18] Rybakov, V. V., Admissibility of Logical Inference Rules (1997), North-Holland: North-Holland Amsterdam · Zbl 0872.03002
[19] Siekmann, J., Unification theory, J. Symbolic Comput., 7, 207-274 (1989) · Zbl 0678.68098
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.