Modal Mantık için Algoritmik Tekabül

Modal mantık formülleri Kripke çatılar üzerinde ikinci mertebeden özellikler ifade etmektedir. Pek çok durumda modal mantık formüllerine karşılık gelen birinci mertebeden mantık formülleri etkili algoritmalar yardımı ile hesaplanmaktadır. Bu alandaki ilk araştırma makalesi, 1973 yılında H. Sahlqvist tarafından yazılan "Modal mantık için birinci ve ikinci dereceden semantikler için tekabül ve tamlık" idi. Yaptığı çalışmada modal mantık formüllerinin belirli bir sınıfını tanımlayarak, bu sınıfın çatılar üzerinde birinci mertebeden koşullar tanımladığını ve bu koşulların da geliştirdiği tekniği yardımı ile modal mantık formüllerine tekabül eden birinci mertebeden formülleri hesaplamıştır. Ancak bir modal mantık formülüne karşılık gelen birinci mertebeden mantık formülü her zaman bulunmayabilir. Bazı durumlarda bir modal mantık formülü ikinci mertebeden mantık formülüne tekabül edebilir. Bu tip durumlarda Sahlqvist tekniği etkinliğini kaybetmektedir. Literatürde bir modal mantık formülüne tekabül eden birinci ve ikinci mertebeden mantık formülünü hesaplamaya yarayan farklı algoritmalar ve teknikler geliştirilmiştir. Bu algoritmalar içinde öne çıkan iki çalışma bulunmaktadır. H. J. Ohlbach ve D. Gabbay tarafından geliştirilen, temeli kısıtlama çözümleme ve tekniğine dayanan SCAN algoritması ve W. Condradie, V. Goranko ve D. Vakarelov tarafından geliştirilen, modal formüller üzerinde direkt olarak çalışan SQEMA algoritmasıdır. Bu çalışmada SCAN ve SQEMA algoritmaları ayrıntılı olarak incelip, karşılaştırması yapılacaktır.

Anahtar Kelimeler:

Modal mantık, SCAN algoritması, SQEMA algoritması

Algorithmic Correspondence for Modal Logic

Modal logic formulas express second-order properties on Kripke frameworks. In many cases, first-order logic formulas corresponding to modal logic formulas are calculated with the help of efficient algorithms. The first research paper in this field was "Correspondence and completeness for first and second order semantics for modal logic" written by H. Sahlqvist in 1975. In his study, he defined a certain class of modal logic formulas, this class defines first-order conditions on frames, and with the help of the technique he developed for these conditions, he calculated first-order formulas corresponding to modal logic formulas. However, a first-order logic formula corresponding to a modal logic formula may not always be found. In some cases, a modal logic formula may correspond to a second-order logic formula. In such cases, the Sahlqvist technique loses its effectiveness. In the literature, different algorithms and techniques have been developed to calculate the first and second order logic formula corresponding to a modal logic formula. There are two prominent studies among these algorithms. One of these algorithms is the SCAN algorithm developed by Ohlbach and Gabbay, which is based on constraint analysis and technique. The other is the SQEMA algorithm developed by Condradie et al., (2006), which works directly on modal formulas. In this study, SCAN and SQEMA algorithms will be examined in detail and compared.

Keywords:

Modal logic, Scan algortihm, Sqema algorithm,

PDF

___

Referans1 Blackburn, P. de Rijke, M., Venema, Y., 2001, Modal Logic, Cambridge University Press.
Referans2 Burris, S. N., 1998, Logic for Mathematics and Computer Science, Prentice Hall.
Referans3 Chellas, B. F., 1980, Modal Logic: An Introduction, Cambridge University Press.
Referans4 Condradie, W. Goranko V., Vakarelov D., 2006, Algorithmic Correspondence and Completeness in Modal Logic. I. Core Algorithm SQEMA, Logical Methods in Computer Science 2 (1;4) 1–26pp.
Referans5 Condradie, W., Goranko V., Vakarelov D., 2006, Algorithmic Correspondence and Completeness in Modal Logic. II. Polyadic and Hybrid Extensions of the Algorithm SQEMA, Journal of Logic and Computation Advance Access.
Referans6 Gabbay, D., Ohlbach H. J., 1992, Quantifier Elimination in Second-Order Predicate Logic, South African Computer Journal, 7: 35–43pp.
Referans7 Goranko V., Vakarelov D., 2002, Sahlqvist formulas Unleashed in Polyadic Modal Languages, Advances in Modal Logic, 3.
Referans8 Hustadt, U., Goranko, V., Vakarelov, D., 2004, SCAN is compeler for all Sahlqvist formulae, In Relational and Kleene-Algebraic Methods in Computer Science.
Referans9 Nonnengart, N., Ohlbach, H. J. , Szalas, A. , 1999, Elimination of Predicate Quantifiers. Logic and Reasoning, 159–181pp.
Referans10 Sahlqvist, H., 1973, Completeness and correspondence in the first and second order semantics for modal logic in Kranger, 110–143pp.
Referans11 Szalas, A. , 1993, On the Correspondence Between Modal and Classical Logic: an Automated Approach, Journal of Logic and Computation, 605–620pp.
Referans12 Vaananen, J., 2001, Second-Order Logic and Foundation of Mathematics, The Bulletin of Symbolic Logic, 7 – 4.