{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T15:06:46Z","timestamp":1726758406576},"reference-count":29,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2006,3,7]],"date-time":"2006-03-07T00:00:00Z","timestamp":1141689600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"Modal formulae express monadic second-order properties on Kripke frames, but\nin many important cases these have first-order equivalents. Computing such\nequivalents is important for both logical and computational reasons. On the\nother hand, canonicity of modal formulae is important, too, because it implies\nframe-completeness of logics axiomatized with canonical formulae.\n Computing a first-order equivalent of a modal formula amounts to elimination\nof second-order quantifiers. Two algorithms have been developed for\nsecond-order quantifier elimination: SCAN, based on constraint resolution, and\nDLS, based on a logical equivalence established by Ackermann.\n In this paper we introduce a new algorithm, SQEMA, for computing first-order\nequivalents (using a modal version of Ackermann's lemma) and, moreover, for\nproving canonicity of modal formulae. Unlike SCAN and DLS, it works directly on\nmodal formulae, thus avoiding Skolemization and the subsequent problem of\nunskolemization. We present the core algorithm and illustrate it with some\nexamples. We then prove its correctness and the canonicity of all formulae on\nwhich the algorithm succeeds. We show that it succeeds not only on all\nSahlqvist formulae, but also on the larger class of inductive formulae,\nintroduced in our earlier papers. Thus, we develop a purely algorithmic\napproach to proving canonical completeness in modal logic and, in particular,\nestablish one of the most general completeness results in modal logic so far.<\/jats:p>","DOI":"10.2168\/lmcs-2(1:5)2006","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:26:35Z","timestamp":1164273995000},"source":"Crossref","is-referenced-by-count":42,"title":["Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA"],"prefix":"10.46298","volume":"Volume 2, Issue 1","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-9906-4132","authenticated-orcid":false,"given":"Willem","family":"Conradie","sequence":"first","affiliation":[]},{"given":"Valentin","family":"Goranko","sequence":"additional","affiliation":[]},{"given":"Dimiter","family":"Vakarelov","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2006,3,7]]},"reference":[{"key":"10.2168\/LMCS-2(1:5)2006_Ackermann","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448035"},{"key":"10.2168\/LMCS-2(1:5)2006_MLBook","doi-asserted-by":"crossref","unstructured":"P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001.","DOI":"10.1017\/CBO9781107050884"},{"key":"10.2168\/LMCS-2(1:5)2006_Chagrova","doi-asserted-by":"publisher","DOI":"10.2307\/2275473"},{"key":"10.2168\/LMCS-2(1:5)2006_CGVAiml5","unstructured":"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). \\textbfAdvances in Modal Logic, vol. 5, Kings College London, 2005, pages 17-51."},{"key":"10.2168\/LMCS-2(1:5)2006_CGVsqema2","doi-asserted-by":"crossref","unstructured":"W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic II: Polyadic and hybrid extensions of the algorithm SQEMA. 2006, submitted.","DOI":"10.2168\/LMCS-2(1:5)2006"},{"key":"10.2168\/LMCS-2(1:5)2006_CGVsqema3","doi-asserted-by":"crossref","unstructured":"W. Conradie and V. Goranko. Algorithmic correspondence and completeness in modal logic III : Semantic extensions of the algorithm SQEMA. 2006, under submission.","DOI":"10.2168\/LMCS-2(1:5)2006"},{"key":"10.2168\/LMCS-2(1:5)2006_CGVsqema4","unstructured":"W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic IV : Recursive and complex extensions of the algorithm SQEMA. In preparation."},{"key":"10.2168\/LMCS-2(1:5)2006_Rij93","unstructured":"M. de Rijke. Extending Modal Logic. PhD thesis, ILLC, University of Amsterdam, ILLC Dissertation Series 1993-4, 1993."},{"key":"10.2168\/LMCS-2(1:5)2006_Szalas1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005722130532"},{"key":"10.2168\/LMCS-2(1:5)2006_Engel","unstructured":"T. Engel. Quantifier Elimination in Second-Order Predicate Logic. Diploma Thesis, MPI, Saarbr\u00fccken, 1996."},{"issue":"1","key":"10.2168\/LMCS-2(1:5)2006_Esakia","first-page":"147","volume":"15","author":"L. L. Esakia.","year":"1974","journal-title":"Soviet Mathematics Doklady, 15(1):147-151, 1974"},{"issue":"6","key":"10.2168\/LMCS-2(1:5)2006_GabbayOlbach","first-page":"607","volume":"22","author":"D. Gabbay, and H.-J. Ohlbach. Quantif","year":"1993","journal-title":"Modal Logic with Names. \\newblock Journal of Philosophical Logic, 22(6):607-636, 1993"},{"key":"10.2168\/LMCS-2(1:5)2006_GorankoVakarelov2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.5.737"},{"key":"10.2168\/LMCS-2(1:5)2006_GorankoVakarelov1","doi-asserted-by":"crossref","unstructured":"V. Goranko, and D. Vakarelov. Sahlqvist Formulas Unleashed in Polyadic Modal Languages. In: F. Wolter et al (eds.). Advances in Modal Logic, vol. 3, World Scientific, Singapore, 2002, pp. 221-240.","DOI":"10.1142\/9789812776471_0012"},{"key":"10.2168\/LMCS-2(1:5)2006_SCANComplete","doi-asserted-by":"crossref","unstructured":"V. Goranko, U. Hustadt, R. Schmidt, and D. Vakarelov. SCAN is complete for all Sahlqvist formulae. In: R. Berghammer, B. M\u00f6ller, and G. Struth (editors).Relational and Kleene-Algebraic Methods in Computer Science (Proc. of RelMiCS 7), LNCS 3051, Springer, 2004, pages 149-162.","DOI":"10.1007\/978-3-540-24771-5_13"},{"key":"10.2168\/LMCS-2(1:5)2006_GorankoVakarelov3","unstructured":"V. Goranko, and D. Vakarelov. Elementary Canonical Formulae: Extending Sahlqvist Theorem, to appear inAnnals of Pure and Applied Logic."},{"key":"10.2168\/LMCS-2(1:5)2006_Gustafsson","unstructured":"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."},{"key":"10.2168\/LMCS-2(1:5)2006_NonnengartSzalas","unstructured":"A. Nonnengart, and A. Szalas. A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. In: E. Orlowska (editor). Logic at Work, Essays dedicated to the memory of Helena Rasiowa. Springer Physica-Verlag, 1998, pages 89-108."},{"key":"10.2168\/LMCS-2(1:5)2006_Szalas2","unstructured":"A. Nonnengart, H.-J. Ohlbach, and A. Szalas. Elimination of Predicate Quantifiers. In: H.-J. Ohlbach and U. Reyle (editors). Logic, Language and Reasoning: Essays in honour of Dov Gabbay, Part I. Kluwer, 1999, pages 159-181."},{"key":"10.2168\/LMCS-2(1:5)2006_Sahlqvist","doi-asserted-by":"crossref","unstructured":"H. Sahlqvist. Correspondence and completeness in the first and second-order semantics for modal logic. In: S. Kanger (editor). Proc. of the 3rd Scandinavian Logic Symposium, Uppsala 1973, North-Holland, Amsterdam, 1975, pages 110-143.","DOI":"10.1016\/S0049-237X(08)70728-6"},{"key":"10.2168\/LMCS-2(1:5)2006_SambinVacarro2","doi-asserted-by":"publisher","DOI":"10.2307\/2274758"},{"key":"10.2168\/LMCS-2(1:5)2006_Simmons","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.1.23"},{"key":"10.2168\/LMCS-2(1:5)2006_Szalas3","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.6.605"},{"key":"10.2168\/LMCS-2(1:5)2006_Szalas4","doi-asserted-by":"crossref","unstructured":"A. Szalas. Second-order quantifier elimination in modal contexts. In: S. Flesca and G. Ianni (editors). JELIA'02, LNAI 2424, Springer-Verlag, 2002, pp. 223-232.","DOI":"10.1007\/3-540-45757-7_19"},{"key":"10.2168\/LMCS-2(1:5)2006_Vakarelov1","unstructured":"D. Vakarelov. Modal definability in languages with a finite number of propositional variables, and a new extension of the Sahlqvist class. In: P. Balbiani, N.-Y. Suzuki, F. Wolter, and M. Zakharyaschev (editors). Advances in Modal Logic, vol. 4, King's College Publications, London, 2003, pp. 495-518."},{"key":"10.2168\/LMCS-2(1:5)2006_Vakarelov2","unstructured":"D. Vakarelov. On a generalization of the Ackermann's Lemma for computing first-order equivalents of modal formulae, abstract. TARSKI Workshop, March 11 - 13, 2003, Toulouse, France."},{"key":"10.2168\/LMCS-2(1:5)2006_Vakarelov3","unstructured":"D. Vakarelov. Modal definability, solving equations in modal algebras and generalizations of the Ackermann lemma. In the Proc. of 5th Panhellenic Logic Symposium, July 25-28, 2005, Athens."},{"key":"10.2168\/LMCS-2(1:5)2006_vanBenthemBook","unstructured":"J. F. A. K. van Benthem. Modal Logic and Classical Logic. Bibliopolis, Napoli, 1983."},{"key":"10.2168\/LMCS-2(1:5)2006_Willard","unstructured":"S. Willard. General Topology. Dover Publications, 2004."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2259\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2259\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:10:53Z","timestamp":1681243853000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2259"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,7]]},"references-count":29,"URL":"https:\/\/doi.org\/10.2168\/lmcs-2(1:5)2006","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0602024","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0602024","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/s11229-015-0834-x","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3,7]]}}}
