Modal lojik ve klasik lojik arasındaki ilişki
Relationship between modal logic and classical logic
Yazar: ZAFER ÖZDEMİR
Danışman: YRD. DOÇ. DR. TAHSİN ÖNER
Ege Üniversitesi / Fen Bilimleri Enstitüsü / Matematik Ana Bilim Dalı
Derece: Yüksek Lisans, 2010
Konu: Matematik = Mathematics

Özet:
Modal formüller Kripke çatılar üzerinde ikinci mertebeden monadic özellikler ifade etmektedir. Pek çok durumda modal formüllere karşılık gelen birinci mertebeden lojik formülleri etkili algoritmalar yardımı ile hesaplanmaktadır. Konuyla ilgili ilk çalışma H. Sahlqvist'in ?Correspondence and completeness in the first and second order semantics for modal logic? isimli makalesidir. Sahlqvist 1973 tarihli makalesinde Sahlqvist formülleri olarak adlandırılan modal lojik 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 Sahlqvist tekniği yardımı ile modal lojik formüllerinden etkili bir biçimde hesaplanabileceğini kanıtlamıştır.Bir modal lojik formülüne karşılık gelen birinci mertebeden lojik formülü her zaman bulunmayabilir. Bazı durumlarda bir modal lojik formülü ikinci mertebe lojik formülüne karşılık gelebilir. Bu tip durumlarda Sahlqvist tekniği etkinliğini kaybetmektedir. Bir modal formüle karşılık gelen birinci ve ikinci mertbe lojik 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 constraint resolution ve tekniğine dayanan SCAN algoritması ve W. Condradie, V. Goranko ve D. Vakarelov tarafından geliştirilen, modal lojik formülleri üzerinde direkt olarak çalışan SQEMA algoritmasıdır.Bu tez giriş bölümü dahil altı ana bölümden oluşmaktadır.İkinci bölümde önermeler lojiğinin ve modal lojiğin temel kavramları tanımlanmıştır.Üçüncü bölümde Sahlqvist formüller sınıfı tanıtılarak Sahlqvist Teoremi verilmiş ve Sahlqvist tekniğinin modal lojik formülleri üzerindeki etkinliği açıklanmıştır.Dördüncü bölümde SCAN algoritmasının temelini oluşturan resolution ve Skolemizasyon tekniği ile ilgili temel tanımlar verilmiş, SCAN algoritmasının adımları ayrıntılı olarak şekilde incelenmiş ve algoritma örneklerle açıklanmıştır. Bölümün sonunda ise algoritmanın Sahlqvist formülleri üzerindeki tamlığı ispatlanmıştır.Beşinci bölümde SQEMA algoritmasının işleyişinde kullanılan temel kavramlar tanımlarla verilmiş, algoritmanın adımları ayrıntılı olarak incelenmiş ve örneklerle açıklanmıştır; bölüm sonunda ise algoritmanın Sahlqvist formülleri üzerindeki tamlığı ispatlanmıştır.Altıncı bölümde Sahlqvist tekniği, SCAN ve SQEMA algoritmaları etkinliklerine göre karşılaştırılmıştır.

Abstract:
Modal formulae express monadic second-order properties on Kripke frames. In many cases modal formulas correspond to first-order formulas computed by influential algorithms. The first research of this area was ?Correspondence and completeness in the first and second order semantics for modal logic? which was written by H. Sahlqvist in 1973. He defined a class of modal formulas which are determined first order conditions on Kripke frames and those conditions can be effectively computed from the modal formulas.Sometimes a first order equivalent of a modal formula doesn?t exist. In some cases a modal formulae can be correspond to a second-order formulae. Under the circumstances Sahlqvist technique loses its effectiveness. Some algorithms and techniques have been developed for computing a first-order or a second-order equivalent of a modal formula. Several algorithms and techniques are introduced but two of them come forward in these algorithms. SCAN, based on constraint resolution technique and SQEMA, works directly on modal formulae.In addition to Introduction Chapter, the thesis consists essentially of The thesis consists of six chapters.Chapter two starts with basic definitions and notions of proposition logic and modal logic.In the chapter three, class of Sahlqvist formulae and Sahlqvist theorem are introduced. Then the effectiveness of Sahlqvist technique is explained on modal formulae.In the chapter four, definitions of resolution and Skolemization technique are introduced which are basis for SCAN algorithm. Then SCAN algorithm is described in great detail, algorithm is illustrated by examples.In the end of this chapter, the completeness of SCAN algorithm is proved with respect to class of Sahlqvist formulae.In the chapter five, basic definitions and notions of SQEMA algorithm are introduced which are used process of this algorithm. The steps of SQEMA algorithm are examined in detail and are explained with examples. In the end of this chapter, the completeness of SQEMA algorithm is proved with respect to class of Sahlqvist algorithm.In the chapter six, Sahlqvist technique, SCAN and SQEMA algorithms are compared with respect to their effectiveness.