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.