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

Revisiting the Satisfiability of Two Variable Logic

丁恩琳(En-Lin Ting)

指導教授 ： 陳偉松

國立臺灣大學/電機資訊學院/資訊工程學研究所/碩士(2018年)

https://doi.org/10.6342/NTU201802560

摘要

含計數量詞的二階邏輯(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 式子的另類技巧，並擴展至其他諸多的本體知識語言。

關鍵字

含計數量詞的二階邏輯 ； 可滿足性 ； Presburger 算數 ； 整數規劃 ； 正則圖

並列摘要

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.

並列關鍵字

two variable logic with counting quantifiers ； satisfiability ； Presburger arithmetics ； integer programming ； regular graphs

參考文獻

[1] A. Church. A note on the entscheidungsproblem. J. Symb. Log., 1(1):40–41, 1936.

[2] A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):pp. 345–363, 1936.

[3] M. Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium ”Rekursive Kombinatorik”held from May 23-28, 1983 at the Institut für Mathematische Logik und Grundlagenforschung der Universität Münster/Westfalen, pages 312–319, 1983.

[4] K. Gödel. Über die vollständigkeit der axiome des logischen funktionenkalküls. Monatshefte für Mathematik und Physik, 36:349–360, 1930.

[5] E. Grädel, P. G. Kolaitis, and M. Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53–69, 1997.