Automated theorem proving by resolution in non-classical logics. (English) Zbl 1130.03010
The main goal of the paper is to find uniform principles, applicable to large classes, which lead to simple and reusable implementations.
The author presents several situations in which nonclassical logics can be translated into tractable and simple fragments of classical logic and resolution can be used successfully for automated theorem proving. The main advantage of such an approach is that it allows one to use existing automated theorem provers.
She shows in this paper that in many interesting situations translations into classical logic allows one to obtain decision procedures of optimal complexity. Such resolution-based decision procedures can be obtained by using refinements of resolution such as ordered resolutionn with selection, or ordered chaining with selection.
The author presents several situations in which nonclassical logics can be translated into tractable and simple fragments of classical logic and resolution can be used successfully for automated theorem proving. The main advantage of such an approach is that it allows one to use existing automated theorem provers.
She shows in this paper that in many interesting situations translations into classical logic allows one to obtain decision procedures of optimal complexity. Such resolution-based decision procedures can be obtained by using refinements of resolution such as ordered resolutionn with selection, or ordered chaining with selection.
Reviewer: Nail Zamov (Kazan)
MSC:
| 03B35 | Mechanization of proofs and logical operations |
References:
| [1] | Anderson, A.R., Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, vol. 1. Princeton University Press, Princeton, NJ (1975) · Zbl 0323.02030 |
| [2] | Andréka, H., van Benthem, J., Németi, I.: Modal languages and bounded fragments of predicate logic. J. Philos. Logic 27, 217–274 (1998) · Zbl 0919.03013 · doi:10.1023/A:1004275029985 |
| [3] | Aguzzoli, S., Ciabattoni, A.: Finiteness of infinite-valued Łukasiewicz logic. J. Logic, Lang. Inf. 9, 5–29 (2000) · Zbl 0951.03024 · doi:10.1023/A:1008311022292 |
| [4] | Andréka, H., Németi, I., Sain, I.: Algebraic logic. In: Handbook of Philosophical Logic, 2nd edn., vol. 2. Kluwer, Dordrecht (2001) · Zbl 1003.03536 |
| [5] | Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Gottlob, G., Walsh, T. (eds) Proceedings of the 18th International Joint Conference on Artificial Intelligence, (IJCAR 2003), pp. 325–330. Morgan Kaufmann, San Mateo, CA (2003) |
| [6] | Baader, F.: The instance problem and the most specific concept in the description logic \({\mathcal E}{\mathcal L}\) w.r.t. terminological cycles with descriptive semantics. In: Günter, A., Kruse, R., Neumann, B. (eds) Proceedings of the 26th Annual German Conference on Artificial Intelligence, (KI 2003). LNAI, vol. 2821, pp. 64–78. Springer, Berlin Heidelberg New York (2003) · Zbl 1274.68450 |
| [7] | Baaz, M., Fermüller, C.G.: Resolution-based theorem proving for many-valued logics. J. Symb. Comput. 19, 353–391 (1995) · Zbl 0839.68091 · doi:10.1006/jsco.1995.1021 |
| [8] | Baaz, M., Fermüller, C.G., Ciabattoni, A.: Herbrand’s theorem for prenex Gödel logic and its consequences for theorem proving. In: Nieuwenhuis, R., Voronkov, A. (eds) Proceedings of LPAR’2001. Lecture Notes in Computer Science, vol. 2250, pp. 201–215. Springer, Berlin Heidelberg New York (2001) · Zbl 1275.03098 |
| [9] | Baaz, M., Fermüller, C.G., Salzer, G.: Automated deduction for many-valued logics. In: Robinson, A., Voronkov, A. (eds) Handbook of Automated Reasoning, vol. II, pp. 1355–1402. Elsevier, Amsterdam, The Netherlands (2001) · Zbl 0992.03015 |
| [10] | Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217 |
| [11] | 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 · doi:10.1145/293347.293352 |
| [12] | Beckert, B., Hähnle, R., Manyà, F.: Transformations between signed and classical clause logic. In: Proceedings of the 29th International Symposium on Multiple-valued Logic (ISMVL’99), Freiburg, Germany, pp. 248–255. IEEE Press, Piscataway, NJ (1999) |
| [13] | Beckert, B., Hähnle, R., Manyà, F.: The 2-SAT problem of regular signed CNF formulas. In: Proceedings of the 30th International Symposium on Multiple-valued Logic (ISMVL’2000), Portland, USA, pp. 331–336. IEEE Press, Piscataway, NJ (2000) |
| [14] | Béjar, R., Hähnle, R., Manyà, F.: A modular reduction of regular logic to classical logic. In: Proceedings if the 31st International Symposium on Multiple-valued Logic (ISMVL’01), Warsaw, Poland, pp. 221–226. IEEE Press, Piscataway, NJ (2001) |
| [15] | Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge, UK (2001) · Zbl 0988.03006 |
| [16] | Burris, S., Sankappanavar, H.P.: A course in universal algebra. In: Graduate Texts in Mathematics. Springer, Berlin Heidelberg New York (1981) · Zbl 0478.08001 |
| [17] | Burris, S.: Polynomial time uniform word problems. Math. Log. Q. 41, 173–182 (1995) · Zbl 0820.08003 · doi:10.1002/malq.19950410204 |
| [18] | Caferra, R., Zabel, N.: An application of many-valued logic to decide propositional S5 formulae: A strategy designed for a parametric tableaux-based theorem prover. In: Artificial Intelligence IV: Methodology, Systems, Applications, pp. 23–32. Elsevier, Amsterdam, The Netherlands (1990) |
| [19] | Dezani-Ciangaglini, M., Frisch, A., Giovannetti, E., Motohama, Y.: The relevance of semantic subtyping. Electronic Notes in Theoretical Computer Science 70(1) (2002) · Zbl 1270.03043 |
| [20] | Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge, UK (1990) · Zbl 0701.06001 |
| [21] | Dummet, M.: A propositional calculus with denumerable matrix. J. Symb. Log. 24(2), 97–106 (1959) · Zbl 0089.24307 · doi:10.2307/2964753 |
| [22] | Dunn, J.M.: Positive modal logic. Stud. Log. 55, 301–317 (1995) · Zbl 0831.03007 · doi:10.1007/BF01061239 |
| [23] | Ganzinger, H., Hustadt, U., Meyer, C., Schmidt, R.A.: A resolution-based decision procedure for extensions of K4. In: Zakharyaschev, M., Segerberg, K., de Rijke, M., Wansing, H. (eds.) Advances in Modal Logic, vol. 119. CSLI Lecture Notes, chapter 9, vol. 2, pp. 225–246. CSLI, Stanford, USA (2001) · Zbl 0993.03017 |
| [24] | Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS’99), pp. 295–303. IEEE Computer Society Press, Los Alamitos, CA (1999) |
| [25] | Goldblatt, R.: Mathematics of modality, vol. 43 of Center for the Study of Language and Information. University of Chicago Press, Chicago, IL (1993) · Zbl 0942.03516 |
| [26] | Ganzinger, H., Sofronie-Stokkermans, V.: Chaining techniques for automated theorem proving in many-valued logics. In: Proceedings of the 30th International Symposium on Multiple-valued Logic (ISMVL’2000), Portland, USA, pp. 337–344. IEEE Press, Piscataway, NJ (2000) |
| [27] | Hähnle, R.: Automated Theorem Proving in Multiple-valued Logics. Oxford University Press, London, UK (1993) · Zbl 0798.03010 |
| [28] | Hähnle, R.: Many-valued logic and mixed integer programming. Ann. Math. Artif. Intell. 12(3,4), 231–264 (1994) · Zbl 0856.03011 · doi:10.1007/BF01530787 |
| [29] | Hähnle, R.: Short conjunctive normal forms in finitely valued logics. J. Log. Comput. 4(6), 905–927 (1994) · Zbl 0818.03003 · doi:10.1093/logcom/4.6.905 |
| [30] | Hähnle, R.: Exploiting data dependencies in many-valued logics. J. Appl. Non-Class. Log. 6(1), 49–69 (1996) · Zbl 0836.03013 |
| [31] | Hähnle, R.: Proof theory of many-valued logic – linear optimization – logic design. Soft Computing – A Fusion of Foundations, Methodologies and Applications 1(3), 107–119 (1997) · doi:10.1007/s005000050012 |
| [32] | Hähnle, R.: Proof theory of many-valued logic – linear optimization – logic design: connections and interactions. Soft Computing – A Fusion of Foundations, Methodologies and Applications 1(3), 107–119 (1997) · doi:10.1007/s005000050012 |
| [33] | Hähnle, R.: Advanced many-valued logics. In: Handbook of Philosophical Logic, vol. 2, pp. 297–395. Kluwer, Dordrecht, 2nd edn. (2001) · Zbl 1003.03522 |
| [34] | Hähnle, R.: Complexity of many-valued logics. In: Fitting, M., Orłowska, E. (eds) Beyond Two: Theory and Applications of Multiple Valued Logic. Studies in Fuzziness and Soft Computing, vol. 114, chapter 3, pp. 211–233. Springer, Berlin (2003) · Zbl 1046.03012 |
| [35] | Hájek, P.: Metamathematics of fuzzy logic. In: Trends in Logic, vol. 4. Kluwer, Dordrecht (1998) · Zbl 0937.03030 |
| [36] | Iturrioz, L., Orłowska, E.: A Kripke-style and relational semantics for logics based on Łukasiewicz algebras. Conference in honour of J. Łukasiewicz, Dublin (1996) · Zbl 1148.03321 |
| [37] | Ishtiaq, S.,O’Hearn, P.: BI as an assertion language for mutable data structures. In: Proceedings of 28th Symposium on Principles of Programming Languages (POPL’01), pp. 14–26. ACM, New York (2001) · Zbl 1323.68077 |
| [38] | Iturrioz, L.: Symmetrical Heyting algebras with operators. Z. Math. Log. Grundl. Math. 29, 33–70 (1983) · Zbl 0537.03049 · doi:10.1002/malq.19830290202 |
| [39] | Kifer, M., Lozinskii, M.: A logic for reasoning with inconsistency. J. Autom. Reason. 9, 179–215 (1992) · Zbl 0807.03019 · doi:10.1007/BF00245460 |
| [40] | Kazakov, Y., de Nivelle, H.: Subsumption of concepts in \({\mathcal F}{\mathcal L}_0\) for (cyclic) terminologies with respect to descriptive semantics is PSPACE-complete. In: Calvanese, D., De Giacomo, G., Franconi, E. (eds) 2003 International Workshop on Description Logics (DL-03), vol. 81 of CEUR Workshop Proceedings, pp. 56–64, University of Rome ”La Sapienza” and Free University of Bolzano/Bozen, CEUR, Rome, Italy (September 2003) |
| [41] | Lu, J., Murray, N.V., Rosenthal, E.: A framework for reasoning in multiple-valued logics. J. Autom. Reason. 21(1), 39–67 (1998) · Zbl 0913.03023 · doi:10.1023/A:1005784309139 |
| [42] | Łukasiewicz, J.: Philosophische Bemerkungen zu mehrwertigen Systemen des Aussagenkalküls. Comptes rendus de la Société des Sciences et Lettres de Varsovie, cl.iii 23, 51–77 (1930) |
| [43] | Manyà, F.: The 2-SAT problem in signed CNF formulas. Multiple-Valued Logic. An International Journal 5 (2000) · Zbl 0992.03014 |
| [44] | McAllester, D., Givan, R., Kozen, D., Witty, C.: Tarskian set constraints. Inf. Comput. 174, 105–131 (2002) · Zbl 1009.03019 · doi:10.1006/inco.2001.2973 |
| [45] | Mundici, D., Olivetti, N.: Resolution and model building in the infinite-valued calculus of Łukasiewicz. Theor. Comp. Sci. 200, 335–366 (1998) · Zbl 0921.03013 · doi:10.1016/S0304-3975(98)00012-7 |
| [46] | Mundici, D.: Satisfiability of many-valued sentential logics is NP-complete. Theor. Comp. Sci. 52, 145–153 (1987) · Zbl 0639.03042 · doi:10.1016/0304-3975(87)90083-1 |
| [47] | Ohlbach, H.J.: Translation methods for non-classical logics: An overview. Bulletin of the IGPL 1(1), 69–89 (1993) · Zbl 0795.03019 · doi:10.1093/jigpal/1.1.69 |
| [48] | Ono, H., Komori, Y.: Logics without the contraction rule. J. Symb. Log. 50, 169–201 (1985) · Zbl 0583.03018 · doi:10.2307/2273798 |
| [49] | Ono, H.: Semantics for substructural logics. In: Schroeder-Heister, P., Došen, K. (eds) Substructural Logics, pp. 259–291. Oxford University Press, London, UK (1993) · Zbl 0941.03522 |
| [50] | Pym, D.J.: The semantics and proof theory of the logic of bunched implications. In: Applied Logics Series, vol. 26. Kluwer, Boston, MA (2002) · Zbl 1068.03001 |
| [51] | Rasiowa, H.: An algebraic approach to non-classical logics. In: Studies in Logic and the Foundations of Mathematics, vol. 78. North Holland, Amsterdam, The Netherlands (1974) · Zbl 0299.02069 |
| [52] | Schmidt, R.A.: Decidability by resolution for propositional modal logics. J. Autom. Reason. 22(4), 379–396 (1999) · Zbl 0924.68178 · doi:10.1023/A:1006043519663 |
| [53] | 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 |
| [54] | Sofronie-Stokkermans, V.: On uniform word problems involving bridging operators on distributive lattices. In: Egly, U., Fermüller, Ch. (eds) Proceedings of TABLEAUX 2002. LNAI, Copenhagen, Denmark, vol. 2381, pp. 235–250. Springer, Berlin Heidelberg New York (2002) · Zbl 1016.06005 |
| [55] | Sofronie-Stokkermans, V.: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators. J. Symb. Comput. 36(6), 891–924 (2003) · Zbl 1043.03013 · doi:10.1016/S0747-7171(03)00069-5 |
| [56] | Urquhart, A.: Many-valued logic. In: Gabbay, D., Guenthner, F. (eds) Handbook of Philosophical Logic, vol. III, pp. 71–116. Reidel, Amsterdam, The Netherlands (1986) · Zbl 0875.03054 |
| [57] | Urquhart, A.: Duality for algebras of relevant logics. Stud. Log. 56(1,2), 263–276 (1996) · Zbl 0844.03032 · doi:10.1007/BF00370149 |
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.
