Algorithmic Correspondence and Completeness in Modal Logic. III. Extensions of the Algorithm SQEMA with Substitutions

• Autorzy: Conradie W. , Goranko V. , Vakarelov D.
• Języki publikacji: EN

Abstrakty

EN

In earlier papers we have introduced an algorithm, SQEMA, for computing first-order equivalents and proving canonicity of modal formulae. However, SQEMA is not complete with respect to the so called complex Sahlqvist formulae. In this paper we, first, introduce the class of complex inductive formulae, which extends both the class of complex Sahlqvist formulae and the class of polyadic inductive formulae, and second, extend SQEMA to SQEMA^sub by allowing suitable substitutions in the process of transformation. We prove the correctness of SQEMA^sub with respect to local equivalence of the input and output formulae and d-persistence of formulae on which the algorithm succeeds, and show that SQEMA^sub is complete with respect to the class of complex inductive formulae.

Słowa kluczowe

EN

SQEMA; correspondence; d-persistence; complex Sahlqvist formulae

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 92, nr 4
• Strony: 307--343
• Opis fizyczny: Bibliogr. 36 poz.

Twórcy

autor

Conradie W.

autor

Goranko V.

autor

Vakarelov D.

• Faculty of Mathematics and Computer Science, Sofia University, Sofia, Bulgaria,

Bibliografia

• [1] W. Ackermann. Untersuchung über das Eliminationsproblem der mathematischen Logic. Mathematische Annalen, 110:390-413, 1935.
• [2] P. Blackburn, M. de Rijke, and Y. Venema.Modal Logic. Cambridge University Press, 2001.
• [3] L. A. Chagrova. An undecidable problem in correspondence theory. Journal of Symbolic Logic, 56:1261-1272, 1991.
• [4] W. Conradie. Completeness and correspondence in hybrid logic via an extension of SQEMA. Electronic Notes in Theoretical Computer Science, 231:175 - 190, 2009. Proceedings of the 5thWorkshop on Methods for Modalities (M4M5 2007).
• [5] W. Conradie, V. Goranko, and D. Vakarelov: Elementary canonical formulae: a survey on syntactic, algorithmic, and model-theoretic aspects, In: R. Schmidt, I. Pratt-Hartmann, M. Reynolds, and H. Wansing (editors). Advances in Modal Logic, vol. 5, Kings College London, 2005, pages 17-51.
• [6] W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic I : The core algorithm SQEMA. Logical Methods in Computer Science, 2(1:5), 2006.
• [7] W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic II. Polyadic and hybrid extensions of the algorithm SQEMA. Journal of Logic and Computation, 16:579-612, 2006.
• [8] W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence in modal logic. V : Recursive extensions of the algorithm SQEMA, 2009, submitted.
• [9] M. de Rijke and Y. Venema. Sahlqvist's Theorem For Boolean Algebras with Operators with an Application to Cylindric Algebras, Studia Logica, 54: 61-78, 1995.
• [10] P. Doherty, W. Łukaszewicz, and A. Szałas, Computing circumscription revisited, Journal of Automated Reasoning, 1997, 18(3):297-336.
• [11] T. Engel. Quantifier Elimination in Second-Order Predicate Logic, Diploma Thesis, MPI, Saarbrücken, 1996.
• [12] D. Gabbay and H.-J. Ohlbach. Quantifier elimination in second-order predicate logic. South African Computer Journal, 7: 35-43, 1992.
• [13] D. M. Gabbay, R. Schmidt, and A. Szałas. Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. Studies in Logic, vol. 12, College Publications, 2008.
• [14] D. Georgiev, T. Tinchev and D. Vakarelov. SQEMA - an algoritm for computing first-order equivalents in modal logic: a computer realization. In: Pioneers of Bulgarian Mathematics, International Conference dedicated to Nicola Obrechkoff and Lubomir Tschakaloff, Sofia, July 8-10, 2006. Abstracts.
• [15] V. Goranko and D. Vakarelov. Sahlqvist Formulae Unleashed in Polyadic Modal Languages, In: F. Wolter et al (eds.), Advances in Modal Logic, vol. 3, World Scientific, Singapore, 2002, pp. 221-240.
• [16] V. Goranko, and D. Vakarelov. Sahlqvist Formulae in Hybrid Polyadic Modal Languages. Journal of Logic and Computation, 11(5):737-254, 2001.
• [17] V. Goranko, and D. Vakarelov. Elementary Canonical Formulae: Extending Sahlqvist Theorem. Annals of Pure and Applied Logic, 141(1-2):180-217, 2006.
• [18] V. Goranko, U. Hustadt, R. Schmidt, and D. Vakarelov. SCAN is complete for all Sahlqvist formulae, in: Relational and Kleene-Algebraic Methods in Computer Science (Proc. of RelMiCS 7), LNCS 3051, Springer, 2004, 149-162.
• [19] J. Gustafsson. An Implementation and Optimization of an Algorithm for Reducing Formulae in Second- Order Logic. Technical Report LiTH-MAT-R-96-04. Dept. of Mathematics, Linkoping University, Sweden, 1996.
• [20] A. Nonnengart and A. Szałas. A fixpoint approach to second-order quantifier elimination with applications to correspondence theory, in: E. Orlowska (ed.), Logic at Work, Essays dedicated to the memory of Helena Rasiowa, Springer Physica-Verlag, 89-108, 1998.
• [21] A. Nonnengart, H.-J. Ohlbach, and A. Szałas, Elimination of Predicate Quantifiers, in: H. J. Ohlbach and U. Reyle (eds.), Logic, Language and Reasoning: Essays in honour of Dov Gabbay, Part I, Kluwer, 1999, 159-181.
• [22] H. Sahlqvist. Correspondence and completeness in the first and second-order semantics for modal logic, in: S. Kanger (ed.), Proc. of the 3rd Scandinavial Logic Symposium, Uppsala 1973, North-Holland, Amsterdam, 1975, 110-143.
• [23] A. Szałas, On the correspondence between modal and classical logic: An automated approach. Journal of Logic and Computation, 3:605-620, 1993.
• [24] A. Szałas, Second-order quantifier elimination in modal contexts, in: S. Flesca and G. Ianni (eds.), JELIA'02, LNAI 2424, Springer-Verlag, 2002, pp. 223-232.
• [25] B. ten Cate, M. Marx, and P. Viana. Hybrid logics with Sahlqvist axioms. Logic Journal of the IGPL, 13(3): 293-300, 2005.
• [26] D. Vakarelov, Modal definability in languages with a finite number of propositional variables, and a new extention of the Sahlqvist class. In: P. Balbiani, N.-Y. Suzuki, F. Wolter, and M. Zakharyaschev (eds), Advances in Modal Logic, vol. 4, King's College Publications, London, 2003, pp. 495-518.
• [27] D. Vakarelov. Exstended Sahlqvist Formulae and Solving Equations in Modal Algebras, Abstract, 12-th International Congress of Logic Methodology and Philosophy of Science, August 7-13, 2003, Oviedo, Spain,Program, p. 33.
• [28] D. Vakarelov, On a generalization of the Ackermann lemma for computing first-order equivalents of modal formulae, abstract, TARSKI Workshop,March 11 - 13, 2003, Toulouse, France.
• [29] D. Vakarelov.Modal definability, solving equations in modal algebras and generalization of the Ackermann lemma. In the Proceedings of 5th Panhellenic Logic Symposium, Athens, July 25-28, 2005, 182-189.
• [30] D. Vakarelov. On a generalization of the Ackermann lemma for computing first-order equivalents of modal formulae. In: Logic Colloquium 2005, July 28- August 5, Athens, Greece, Abstracts, p. 123.
• [31] D. Vakarelov. Solving recursive equations in complete modal algebras with applications to modal definability. In: Pioneers of BulgarianMathematics, International Conference dedicated to Nicola Obrechkoff and Lubomir Tschakaloff, Sofia, July 8-10, 2006. Abstracts.
• [32] D. Vakarelov, A recursive generalizations of Ackermann lemma with applications to μ-definability. In 6th Panhellenic Logic Symposium PLS-2007, 5-8 July, Volos, Greece, Extended abstacts, G.Kaouri and S. Zahos Eds, pp. 133-137.
• [33] J. F. A. K. van Benthem. Modal Logic and Classical Logic. Bibliopolis, Napoli, 1983.
• [34] J. F. A. K. van Benthem. Some Correspondence Results in Modal Logic, Tech. Report 74-05,Mathematisch Instituut, Univ. van Amsterdam, 1974.
• [35] J. F. A. K. van Benthem. Minimal predicates, fixed-points, and definability. Journal of Symbolic Logic, 70:3:696-712, 2005.
• [36] J. F. A. K. van Benthem. Modal frame correspondence and fixed-points. Studia Logica, 83: 133-155, 2006.