We are going to analyze the time complexity of obtaining PREBϕfrom aRCS sentence ϕ.
Let r be the number of distinct predicates and k be the largest quantifier in ϕ. We denote the length of a formula ψ by|ψ|. Define the length of a formula to be the summation of the length of all the symbols in it with repeats, and the length of a formula ψ is defined inductively as follows:
• |z = z| = O(1) where z ranges over {x, y}.
• |R(z, z)| = O(log r) where z ranges over {x, y} and R is an arbitrary binary pred-icate.
• |P (z, z)| = O(log r) where z ranges over {x, y} and P is an arbitrary unary
variables in ϕ. For the subformula FORALL2( ¯X), it takes 2O(r)time to find the maximal subsetS of E such that S |= (¬β ∧ x ̸= y), and the
To analyze the part CON( ¯X), we start with analyzing its subformulas. In particular, we analyze BiREG, and REG has the same complexity by symmetry. Observe that equa-tion 5.2, for each BiREGD
Ti→Tj,←D Ti→Tj− ( ¯XTi, ¯XTj), the subscripted matrices are of size 2|E| × |G|, and each entry is an integer between 1 to k. First, for the base case defined as in equation 4.2 where the subscripted matrices of BiREG are of size 1× |G|, we can easily see the length of first two lines is O(|G|×log(|T ||G|)) = 22O(r log log k)
, and the largest constant in them is no greater than 2k2|G|2+ 3 = 22O(r log log k)
. Now, for the third line, since the length of ¯XTi, ¯XTj are|G| = 22O(r log log k) base case, the length of the formula is bounded by 222O(r log log k)
. Now we consider the in-ductive construction of BiREG for matrices with 2|E| rows. Observe that, by equation 4.3, in each induction step, the total length is the summation of H(C,D) and the multiplication of|E| and the length of the previous step. Like the base case, we can conclude the largest
constant is also no greater than 2×2|E|×k2(|G|×2|E|)2+3×2|E| = 22O(r log log k)
, the length of HC,Dis also 222O(r log log k)
, and thence the total length of BiREGD
Ti→Tj,←D Ti→Tj− ( ¯XTi, ¯XTj) is bounded by 22O(r log log k)
× 222O(r log log k)
= 222O(r log log k)
.
Therefore, the length of PREBϕ is bounded by 2O(r) × (2O(r))2 × 222O(r log log k)
= 222O(r log log k)
, and thus bounded by 222O(|ϕ|). Moreover, the largest constant in PREBϕ is bounded by 22O(|ϕ|). With nondeterminism, however, for each HC,D, we can simply guess the correct ( ¯M , ¯N ) ∈ HC,D and guess the order of rows in the induction step of equa-tion 4.3, and therefore the length of PREBϕshould be bounded by 22O(|ϕ|).
Observe that FORALL1( ¯X)∧ FORALL2( ¯X)∧ CON( ¯X) is quantifier free and has length less than |PREBϕ|. Therefore, by applying theorem 3.3.3. our algorithm runs in nondeterministic double exponential time, which is stated formally in the following theorem.
Theorem 5.3.1 There is a constant c and a nondeterministic algorithmA such that on inputRCS sentence ϕ, A decide whether ϕ is (finitely) satisfiable in time O(22c|ϕ|).
Chapter 6
Concluding remarks
In this thesis, we present new decision procedures for the satisfiability and finite satis-fiability problems for RCS formulas. The decision procedures, which are based on the technique by Kopczyński and Tan [9], are simple compared to existing procedures. It is by converting anRCS formula into an existential Presburger formula. Furthermore, some interesting remarks can be derived from our approach.
First, note that in PREBϕwe can assume the part FORALL1( ¯X)∧ FORALL2( ¯X)∧ CON( ¯X) does not contain any disjunction by guessing via nondeterminism as in theo-rem 3.3.3. Thus, the length of the resulting formula is still 22O(|ϕ|), and the largest constant a is no greater than 22O(|ϕ|) by the analysis in section 5.3.
Let us denote by φ( ¯X) the part FORALL1( ¯X)∧ FORALL2( ¯X)∧ CON( ¯X) (which is without any disjunction). By corollary 3.3.2, if there exists a solution ¯X ∈ N|T ||G|
for φ( ¯X), there is also some solution ¯Y in{0, 1, . . . , (|T ||G| + |φ|)(|φ| · a)(2|φ|+1)}|T ||G|
such that φ( ¯Y ) holds. Notice that (|T ||G| + |φ|)(|φ| · a)(2|φ|+1) = (22O(|ϕ|))22O(|ϕ|) = 222O(|ϕ|) and |T ||G| = 22O(|ϕ|). Therefore, if ϕ has a finite model, i.e., there is a solution for FORALL1( ¯X)∧ FORALL2( ¯X)∧ CON( ¯X) inN|T ||G|, then there is also a solution Y such that¯ ∑
Y = 222O(|ϕ|) × 22O(|ϕ|) = 222O(|ϕ|), which implies there is a model of size 222O(|ϕ|) for ϕ. This observation is stated formally as the following corollary.
Corollary 6.0.1 There is a constant c such that for everyRCS sentence ϕ, ϕ has a finite model if and only if ϕ has a model of size O(222c|ϕ|).
Second, note that we can also derive the decidability of checking whether the spectrum of anRCS formula is infinite via the following formula:
φ := ∀y∃ ¯X (
FORALL1( ¯X)∧ FORALL2( ¯X)∧ CON( ¯X)∧∑
X¯ ≥ y) ,
Since satisfiability of Presburger formula is decidable [12, 16], we obtain the following corollary.
Corollary 6.0.2 Checking whether anRCS sentence has a infinite spectrum is decidable.
For future work, we plan to extend our result to the whole C2 class and provide an alternative technique to reason about C2formula, thus many other ontology languages.
Bibliography
[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 prob-lem (with implications for logical decision probprob-lems). In Logic and Machines: De-cision Problems and Complexity, Proceedings of the Symposium ”Rekursive Kom-binatorik” 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.
[6] E. Grädel and M. Otto. On logics with two variables. Theor. Comput. Sci., 224(1-2):73–113, 1999.
[7] E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 306–317, 1997.
[8] A. Kahr, E. Moore, and H. Wang. Entscheidungsproblem reduced to the∀∃∀ case.
Proc. Nat. Acad. Sci. U.S.A., 48:365–377, 1962.
[9] E. Kopczyński and T. Tan. Regular graphs and the spectra of two-variable logic with counting. SIAM J. Comput., 44(3):786–818, 2015.
[10] H. R. Lewis. Complexity results for classes of quantificational formulas. J. Comput.
Syst. Sci., 21(3):317–353, 1980.
[11] M. Mortimer. On languages with two variables. Math. Log. Q., 21(1):135–140, 1975.
[12] D. C. Oppen. A 222p(n) upper bound on the complexity of presburger arithmetic.
Journal of Computer and System Sciences, 16(3):323–332, 1978.
[13] L. Pacholski, W. Szwast, and L. Tendera. Complexity results for first-order two-variable logic with counting. SIAM J. Comput., 29(4):1083–1117, 2000.
[14] C. H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765–768, 1981.
[15] I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quanti-fiers. Journal of Logic, Language and Information, 14(3):369–395, 2005.
[16] M. Presburger. Über de vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, pages 92–101. Warsaw, 1927.
[17] D. Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27:377, 1962.
[18] B. A. Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. Doklady Akademii Nauk SSSR, 70:569–572, 1950. English translation in [19].
[19] B. A. Trakhtenbrot. Impossibility of an algorithm for the decision problem in finite classes. American Mathematical Society Translations, 23:1–6, 1950.
[20] A. M. Turing. On computable numbers, with an application to the entschei-dungsproblem. Proceedings of the London Mathematical Society, 42:230–265, 1936.