×

Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators. (English) Zbl 1043.03013

Summary: We establish a link between the satisfiability of universal sentences with respect to classes of distributive lattices with operators and their satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal theory of some such classes. In particular, we obtain exponential space and time decision procedures for the universal clause theory of (i) the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, and (ii) the class of all bounded distributive lattices with operators, and a doubly-exponential time decision procedure for the universal clause theory of the class of all Heyting algebras.

MSC:

03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
06D20 Heyting algebras (lattice-theoretic aspects)

Software:

SPASS; FLOTTER
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson, A. R.; Belnap, N. D., Entailment—The Logic of Relevance and Necessity (1975), Princeton University Press · Zbl 0323.02030
[2] Andréka, H.; van Benthem, J.; Németi, I., Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic, 27, 217-274 (1998) · Zbl 0919.03013
[3] Bachmair, L.; Ganzinger, H., Ordered chaining calculi for first-order theories of transitive relations, Journal of the ACM, 45, 6, 1007-1049 (1998) · Zbl 1065.68615
[4] Bachmair, L.; Ganzinger, H., Resolution theorem proving, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. 1 (2001), North Holland), 19-100, (Chapter 2) · Zbl 0993.03008
[5] Bachmair, L.; Ganzinger, H.; Waldmann, U., Set constraints are the monadic class, (Eighth Annual IEEE Symposium on Logic in Computer Science (1993), IEEE Computer Society Press), 75-83
[6] Blyth, T. S.; Varlet, J. C., Ockham Algebras (1994), Oxford Science Publications · Zbl 0835.06011
[7] Burris, S.; Sankappanavar, H. P., A Course in Universal Algebra, Graduate Texts in Mathematics (1981), Springer Verlag · Zbl 0478.08001
[8] Cosmadakis, S.S., 1985. Equational theories and database constraints. Ph.D. thesis. Massachusetts Institute of Technology; Cosmadakis, S.S., 1985. Equational theories and database constraints. Ph.D. thesis. Massachusetts Institute of Technology · Zbl 0576.68078
[9] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (1990), Cambridge University Press · Zbl 0701.06001
[10] de Nivelle H., 2001. Translation from S4 into the guarded fragment and the 2-variable fragment. Workshop on Tableaux for Dynamic and Modal Logics; de Nivelle H., 2001. Translation from S4 into the guarded fragment and the 2-variable fragment. Workshop on Tableaux for Dynamic and Modal Logics
[11] Demri, S., 2001. Personal communication; Demri, S., 2001. Personal communication
[12] Demri, S.; Goré, R., An \(O((n· logn)^3)\)-time transformation from Grz into decidable fragments of classical first-order logic, (Caferra, R.; Salzer, G., Automated Deduction in Classical and Non-classical LogicsProceedings of FTP’98. Automated Deduction in Classical and Non-classical LogicsProceedings of FTP’98, LNAI, vol. 1761 (2000), Springer Verlag) · Zbl 0956.03026
[13] Dunn, J. M., Partial gaggles applied to logics with restricted structural rules, (Schroeder-Heister, P.; Dosen, K., Substructural Logics. Studies in Logic and Computation, vol. 2 (1993), Oxford Science Publisher), 63-108 · Zbl 0941.03521
[14] Fermüller, C.; Leitsch, A.; Tammet, T.; Zamov, N., Resolution Method for the Decision Problem, LNCS, vol. 679 (1993), Springer Verlag · Zbl 0789.03013
[15] Ganzinger, H.; de Nivelle, H., A superposition decision procedure for the guarded fragment with equality, (Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (1999), IEEE Computer Society Press), 295-303
[16] Ganzinger, H.; Hustadt, U.; Meyer, C.; Schmidt, R. A., A resolution-based decision procedure for extensions of K4, (Zakharyaschev, M.; Segerberg, K.; de Rijke, M.; Wansing, H., Advances in Modal Logic. Advances in Modal Logic, CSLI Lecture Notes, vol. 119, vol. 2 (2001), CSLI: CSLI Stanford, USA), 225-246, (Chapter 9) · Zbl 0993.03017
[17] Ganzinger, H.; Meyer, C.; Veanes, M., The two-variable guarded fragment with transitive relations, (Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (1999), IEEE Computer Society Press), 24-34
[18] Gehrke, M.; Jónsson, B., Bounded distributive lattices with operators, Mathematica Japonica, 40, 2, 207-215 (1994) · Zbl 0855.06009
[19] Gehrke, M.; Jónsson, B., Monotone bounded distributive lattice expansions, Mathematica Japonica, 52, 2, 197-213 (2000) · Zbl 0972.06005
[20] Goldblatt, R., Varieties of complex algebras, Annals of Pure and Applied Logic, 44, 3, 153-301 (1989)
[21] Grädel, E., On the restraining power of guards, The Journal of Symbolic Logic, 64, 1719-1742 (1999) · Zbl 0958.03027
[22] Halmos, P., Algebraic logic I. Monadic Boolean algebras, Compositio Mathematicae, 12, 217-249 (1955)
[23] Hunt, H. B.; Rosenkrantz, D. J.; Bloniarz, P. A., On the computational complexity of algebra of lattices, SIAM Journal of Computation, 16, 1, 129-148 (1987) · Zbl 0642.06005
[24] Jónsson, B.; Tarski, A., Boolean algebras with operators, Part I, American Journal of Mathematics, 73, 891-939 (1951) · Zbl 0045.31505
[25] Jónsson, B.; Tarski, A., Boolean algebras with operators, Part II, American Journal of Mathematics, 74, 127-162 (1952) · Zbl 0045.31601
[26] McAllester, D.; Givan, R.; Kozen, D.; Witty, C., Tarskian set constraints, (Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (1996), IEEE Computer Society Press), 138-151
[27] McKinsey, J. C.C., The decision problem for some classes of sentences without quantifiers, The Journal of Symbolic Logic, 8, 3, 61-76 (1943) · Zbl 0063.03864
[28] Mielniczuk, P.; Pacholski, L., Tarskian set constraints are in NEXPTIME, (Brim, L.; Gruska, J.; Zlatuska, J., Proceedings of MFCS’98. Proceedings of MFCS’98, LNCS, vol. 1450 (1998), Springer Verlag), 589-596 · Zbl 0914.03050
[29] Ohlbach, H. J., Translation methods for non-classical logics: an overview, Bulletin of the IGPL, 1, 1, 69-89 (1993) · Zbl 0795.03019
[30] Ohlbach, H. J.; Nonnengart, A.; de Rijke, M.; Gabbay, D., Encoding two-valued nonclassical logics in classic logic, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier: Elsevier Amsterdam, Netherlands), 1403-1485, (Chapter 21) · Zbl 0992.03019
[31] Priestley, H. A., Representation of distributive lattices by means of ordered Stone spaces, Bulletin of the London Mathematical Society, 2, 186-190 (1970) · Zbl 0201.01802
[32] Priestley, H. A., Ordered sets and duality for distributive lattices, Annals of Discrete Mathematics, 23, 39-60 (1984) · Zbl 0557.06007
[33] Sofronie-Stokkermans, V., 1997. Fibered structures and applications to automated theorem proving in certain classes of finitely-valued logics and to modeling interacting systems. Ph.D. thesis. RISC-Linz Report Series 97-16, RISC-Linz, J. Kepler University Linz, Austria; Sofronie-Stokkermans, V., 1997. Fibered structures and applications to automated theorem proving in certain classes of finitely-valued logics and to modeling interacting systems. Ph.D. thesis. RISC-Linz Report Series 97-16, RISC-Linz, J. Kepler University Linz, Austria
[34] Sofronie-Stokkermans, V., On the universal theory of varieties of distributive lattices with operators: Some decidability and complexity results, (Proceedings of the 16th International Conference on Automated Deduction. Proceedings of the 16th International Conference on Automated Deduction, LNAI, vol. 1632 (1999), Springer Verlag), 157-171 · Zbl 0938.06005
[35] Sofronie-Stokkermans, V., Representation theorems and automated theorem proving in non-classical logics, (Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (1999), IEEE Computer Society), 242-247
[36] Sofronie-Stokkermans, V., Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I, Studia Logica, 64, 1, 93-132 (2000) · Zbl 0948.06009
[37] Sofronie-Stokkermans, V., Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics II, Studia Logica, 64, 2, 151-172 (2000) · Zbl 0955.03038
[38] Sofronie-Stokkermans, V., Automated theorem proving by resolution for finitely-valued logics based on distributive lattices with operators, Multiple-Valued Logic—An International Journal, 6, 3-4, 289-344 (2001) · Zbl 1019.03003
[39] Sofronie-Stokkermans, V., 2002. Representation theorems and the semantics of non-classical logics, and applications to automated theorem proving. In: Fitting, M., Orlowska, E. (Eds.), Beyond Two: Theory and Applications of Multiple Valued Logic. Studies in Fuzziness and Soft Computing, vol. 114. Springer, Berlin, pp. 59-100 (Chapter 3); Sofronie-Stokkermans, V., 2002. Representation theorems and the semantics of non-classical logics, and applications to automated theorem proving. In: Fitting, M., Orlowska, E. (Eds.), Beyond Two: Theory and Applications of Multiple Valued Logic. Studies in Fuzziness and Soft Computing, vol. 114. Springer, Berlin, pp. 59-100 (Chapter 3) · Zbl 1042.03013
[40] Struth, G., 1998. Canonical transformations in algebra, universal algebra, and logic. Ph.D. thesis. Max-Planck-Institut für Informatik, Saarbrücken; Struth, G., 1998. Canonical transformations in algebra, universal algebra, and logic. Ph.D. thesis. Max-Planck-Institut für Informatik, Saarbrücken
[41] Szwast, W.; Tendera, L., On the decision problem for the guarded fragment with transitivity, (Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (2001), IEEE Computer Society), 147-156
[42] Weidenbach, Ch.; Gaede, B.; Rock, G., SPASS & FLOTTER version 0.42, (McRobie, M. A.; Slaney, J. K., Proceedings of the 13th International Conference on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction, LNCS, vol. 1104 (1996), Springer Verlag), 141-145 · Zbl 1412.68267
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.