On the Satisfiability Problem for a 4-level Quantified Syllogistic and Some Applications to Modal Logic

• Autorzy: Cantone D. , Asmundo M. N.
• Języki publikacji: EN

Abstrakty

EN

We introduce a multi-sorted stratified syllogistic, called 4LQSR, admitting variables of four sorts and a restricted form of quantification over variables of the first three sorts, and prove that it has a solvable satisfiability problem by showing that it enjoys a small model property. Then, we consider the fragments (4LQSR)h of 4LQSR, consisting of 4LQSR-formulae whose quantifier prefixes have length bounded by h ≥⃒ 2 and satisfying certain additional syntactical constraints, and prove that each of them has an NP-complete satisfiability problem. Finally we show that the modal logic K45 can be expressed in (4LQSR)3.

Słowa kluczowe

EN

syllogism; problem solving; satisfiability; variables logic; predicate calculus; mathematical proofs

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 124, nr 4
• Strony: 427--448
• Opis fizyczny: Bibliogr. 17 poz.

Twórcy

autor

Cantone D.

• Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125 Catania, Italy

autor

Asmundo M. N.

• Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125 Catania, Italy

Bibliografia

• [1] J. Barwise andL. Moss. Vicious circles. Vol. 60 of CSLI Lecture notes. CSLI, Stanford, CA, 1996.
• [2] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, Cambridge Tracts in Theoretical Computer Science, 2001.
• [3] D. Cantone. Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators. Journal of Automated Reasoning, volume 7, number 2, pages 193-230, Kluwer Academic Publishers, Hingham, MA, USA, 1991.
• [4] D. Cantone and V. Cutello. A decidable fragment of the elementary theory of relations and some applications. In ISSAC ’90: Proceedings of the International Symposium on Symbolic and Algebraic Computation, pages 24-29, New York, NY, USA, 1990. ACM Press.
• [5] D. Cantone and V. Cutello. Decision procedures for stratified set-theoretic syllogistics. In Manuel Bronstein, editor, Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, ISSAC’93 (Kiev, Ukraine, July 6-8, 1993), pages 105-110, New York, 1993. ACM Press.
• [6] D. Cantone, V. Cutello, and J. T. Schwartz. Decision problems for Tarski and Presburger arithmetics extended with sets. In CSL ’90: Proceedings of the 4th Workshop on Computer Science Logic, pages 95-109, London, UK, 1991. Springer-Verlag.
• [7] D. Cantone and A. Ferro Techniques of computable set theory with applications to proof verification. Comm. PureAppl. Math., pages 901-945, vol. XLVIII, 1995. Wiley.
• [8] D. Cantone, A. Ferro, and E. Omodeo. Computable set theory. Clarendon Press, New York, NY, USA, 1989.
• [9] D. Cantone and M. Nicolosi Asmundo. On the satisfiability problem for a 3-level quantified syllogistic with an application to modal logic. arXiv:1304.2412 [cs:LO], 2013.
• [10] D. Cantone and M. Nicolosi Asmundo. On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic (extended version). arXiv:1209.1943 [cs:LO], 2012.
• [11] D. Cantone, E. Omodeo, and A. Policriti. Set Theory for Computing - From decision procedures to declarative programming with sets. Springer-Verlag, Texts and Monographs in Computer Science, 2001.
• [12] G. D’Agostino, A. Montanari, and A. Policriti. A set-theoretic translation method for polymodal logics. Journal of Automated Reasoning, 3(15): 317-337, 1995.
• [13] N. Dershowitz and J. P. Jouannaud. Rewrite Systems. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), 243-320, 1990.
• [14] A. Ferro and E.G. Omodeo. An efficient validity test for formulae in extensional two-level syllogistic. Le Matematiche, 33:130-137, 1978.
• [15] A. Formisano, E. Omodeo, and A. Policriti. Three-variable statements of set-pairing. Theoretical Computer Science, 322(1), 147-173, 2004.
• [16] R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal of Computing, 6: 467-480, 1977.
• [17] A. Pietruszczak. Simplified Kripke style semantics for modal logics K45, KB4 and KD45. Bulletin of the Section of Logic. 38(3/4):163-171, 2009.