回顧雙變量邏輯之可滿足性

Abstract

含計數量詞的二階邏輯(C2) 有著許多應用，特別像是本體知識語言的應用，例如用於語意網的OWL。一個著名的結果是：C2 的可滿足性問題可以在非確定性指數時間(NEXPTIME) 內決定，而且這樣的複雜度是最佳的。然而，目前已知的解決技巧較為複雜，通常必須去猜測一個滿足目標式子結構或表示方法，而導致難以實作。 在這篇論文中，我們關注於具有反向關係封閉性並且是Scott’s 正規型態的C2 句子(RCS)。直觀上，如果一個句子φ 是Scott’s 正規型態而且其使用的二元關係具有反向封閉性，φ 就屬於RCS。我們基於Kopczyński 和Tan 的技巧[9]，針對RCS 的可滿足性問題及有限可滿足性問題提出一個新的決策程序，利用將RCS 的式子轉換成Presburger 的存在量化式來解決問題。雖然此方法的時間複雜度比最佳時間高：2-NEXPTIME，但其有幾個優勢： 1. 刻劃出RCS 式子模型的特性，亦即任一RCS 式子的模型皆是由正則圖及二分正則圖組成。 2. 顯示出一RCS 式子的頻譜是否為有限是可決定的。 3. 此方法為解決可滿足性問題及有限可滿足性問題的簡單決策程序。 當原式為Scott’s 正規型態並且詞彙表固定時，我們演算法的時間複雜度為NEXPTIME。我們期待我們的結果能提供討論C2 式子的另類技巧，並擴展至其他諸多的本體知識語言。

Two variable logic with counting quantifiers (C2) has found many applications, especially in ontology language such as OWL used in semantic web. It is well known that the satisfiability problem for C2 is decidable in nondeterministic exponential time (NEXPTIME), and the complexity is optimal. However, the known techniques are quite complicated and they typically involve guessing a structure or a representation that satisfies the input formula, which can be hard to implement. In this thesis, we consider a subclass of C2 formulas, which we call Reversal closed C2 formulas in Scott’s normal form (RCS). Intuitively, a C2 formula φ is in RCS, if it is in Scott’s normal form and the binary relations used in φ are closed under reversal. We present a decision procedure for the satisfiability and finite satisfiability problems for RCS formulas, which is based on the technique by Kopczyński and Tan [9]. Our approach is by converting an RCS formula into an existential Presburger formula. Though the complexity is higher: 2-NEXPTIME (double exponential time), it has a few advantages: 1. It provides a characterization of models of RCS formulas, i.e., every model of an RCS formula is a collection of regular digraphs and biregular graphs. 2. It implies the decidability of checking whether the spectrum of an RCS formula is infinite. 3. It gives simple decision procedures for satisfiability and finite satisfiability problems. When the input is in Scott’s normal form and the vocabulary is fixed, our algorithm yields time complexity NEXPTIME. We hope that our result can be used to provide an alternative technique to reason about C2 formula, thus many other ontology languages.