Translating First-Order Theories into Logic Programs

1 Introduction

For a knowledge representation language, the encoding naturalness and implementation efficiency may be regarded as the two faces of a coin. For instance, higher-order logic is natural to represent almost all kinds of mathematical knowledge, but no practicable solver is available; on the other hand, logic programming can be implemented efficiently, which is obviously achieved at the expense of its naturalness to represent knowledge. It is a challenging task to design a language with a smart tradeoff between these two aspects.

An appropriate candidate for such a language may be the first-order language under stable model semantics [Ferraris et al., 2011; Lin and Zhou, 2011], which provides a unified framework for answer set programming (ASP), a flourishing paradigm of declarative programming emerged over the last decade. First-order quantifiers are introduced so that more flexible ways for encoding become possible. Interestingly, with this language, we can easily represent a class of knowledge for which no natural encodings in logic programs are known. 1 However, this also presents a challenge to develop an answer set solver for first-order theories, which is the main task of this paper. Another language that we will consider is first-order circumscription [McCarthy, 1980], a well-known non-monotonic formalism for knowledge representation.

The main contributions of this paper are as follows. Firstly, we show how first-order theories under stable model semantics over finite structures can be reduced to logic programs, which enables us to compute them by using existing answer set solvers; we also prove that introducing auxiliary predicates in the reduction is essential. Secondly, we discover an embedding of circumscription into stable model semantics involving no auxiliary predicates. With such an embedding, we can then compute first-order theories of circumscription over finite structures via answer set programming. Finally, by undertaking some experiments, we demonstrate the effectiveness of our approach in computing some hard problems beyond NP. As far as we know, under either stable model semantics or circumscription, our approach is the first one to compute arbitrary first-order theories over finite structures.

1 For details, please refer to Section 5 of this paper.

2 Preliminaries

We assume vocabularies are finite sets of predicate constants and function constants. Every constant is equipped with a natural number, its arity. For technical reasons, following constants are reserved: a binary predicate constant succ, and two nullary function constants (i.e. individual constants) min and max. All these constants are called successor constants.

Logic symbols are defined as usual, including a countable set of predicate variables and a countable set of individual variables. Predicate constants and variables are simply called predicates if no confusion occurs. Terms, formulae, and sentences of a vocabulary σ (or shortly, σ-terms, σ-formulae, and σ-sentences) are built from σ, equality, and variables in a standard way. The only thing which may be special is that we treat ¬ϕ as a shorthand of ϕ → ⊥, and ϕ ↔ ψ as the conjunction of ϕ → ψ and ψ → ϕ. A (finite) first-order theory is a (finite) set of first-order sentences. Clearly, a finite first-order theory can be regarded as a first-order sentence, i.e., a finite conjunction of the sentences in that set. A first-order formula is in prenex normal form if it is of the formQ1x1 · · ·Qnxnϕ, where Qi(i = 1, . . . , n) is ∀ or ∃ and ϕ is quantifier-free. Given a natural number n, a Σn-formula (Πn-formula) is a first-order formula in prenex normal form that has a prefix of n alternating blocks of quantifiers starting with an existential (universal) block, followed by a quantifier-free formula.

Every structure A of a vocabulary σ (or shortly, σ-structure A) is accompanied by a nonempty set A, the domain of A, and interprets each n-ary predicate constant P of σ as an n-ary relation A(P ) on A, and interprets each n-ary function constant f of σ as an n-ary function A(f) on A. Every assignment in a structure A is a function α that maps each individual variable to an element of A and that maps each n-ary predicate variable to an n-ary relation on A. Given a σ-formula ϕ and an assignment α in A, we write A |= ϕ[α] if α satisfies ϕ in A in the standard way. Specially, if ϕ is a sentence, [α] may be dropped, and A is said to be a model of ϕ, or in other words, A satisfies ϕ. Let ϕ(¯x) be a formula with free variables ¯x. We simply write A |= ϕ(¯a) if there is an assignment α in A that assigns ¯x to ¯a and that satisfies ϕ(¯x) in A.

A structure is finite if its domain is finite. A finite structure A is a successor structure if following statements hold: (i) the vocabulary σ of A contains all the successor constants; and (ii) there is an isomorphism between A and the number system Zn (where n = |A|) such that A(succ) is corresponding to the successor relation on Zn (i.e. the set {0, . . . , n - 1}), and A(min) and A(max) are corresponding to 0 and n - 1 respectively. A restriction of a structure A to a vocabulary σ, written by A↾σ, is the structure obtained from A by discarding all interpretations for constants which do not belong to σ. Furthermore, a σ-structure A is said to be an expansion of a σ0-structure B if σ ⊇ σ0 and B is a restriction of A to σ0.

2.1 Circumscription

We follow the notion of parallel circumscription in [Lifschitz, 1985]. 2 Let ϕ be a first-order sentence and ¯ P a tuple of predicate constants. For each predicate constant P that occurs in ¯ P (or simply P ∈ ¯ P) we introduce a new predicate variable XP of the same arity, and let ¯X¯ P be short for the tuple (XP )P ∈ ¯ P . Moreover, we write ¯X¯ P = ¯ P for the conjunction of formulae ∀¯x(XP (¯x) ↔ P(¯x)) for all predicate constants P ∈ ¯ P, and write ¯X¯ P ≤ ¯ P for the conjunction of formulae ∀¯x(XP (¯x) → P(¯x)) for all P ∈ ¯ P. The circumscription CIRC(ϕ; ¯ P) for ϕ is defined to be the second-order sentence ϕ ∧ ∀ ¯X ¯ P ( ¯X¯ P < ¯ P → ¬ϕ( ¯X¯ P )), where ϕ( ¯X¯ P ) is the formula obtained from ϕ by substituting the variables ¯X ¯ P for the constants ¯ P, and ¯X¯ P < ¯ P short for the formula ( ¯X¯ P ≤ ¯ P) ∧ ¬( ¯X¯ P = ¯ P). A structure A is called a ¯ P - minimal model of ϕ if it is a model of CIRC(ϕ; ¯ P ).

2.2 Stable Models

Similarly, stable model semantics is defined by a syntax translation SM. Given a first-order sentence ϕ and a tuple ¯ P of predicate constants, let SM(ϕ; ¯ P) stand for the second-order sentence ϕ ∧ ∀ ¯X ¯ P ( ¯X¯ P < ¯ P → ¬St(ϕ; ¯ P)), where the formula St(ϕ; ¯ P) is defined recursively as follows:

• St(P(¯ t); ¯ P ) = XP (¯ t) if P is a predicate constant in ¯ P .
• St(ψ; ¯ P) = ψ if ψ is an atom not in the previous case.

A structure A is called a ¯ P-stable model of ϕ if it is a model of SM(ϕ; ¯ P). A predicate constant is said to be intensional if it occurs in ¯ P. Otherwise, it is extensional. An extensional database of ϕ is a σ-structure such that σ consists of the set of all the extensional predicate constants and function constants. For more information, please refer to [Ferraris et al., 2011].

2 Since they can be efficiently eliminated by a method in [Cadoli et al., 1992], we will not consider varying predicates in this paper.

3 Quantifier Elimination

In classical logic, first-order existential quantifiers can be easily removed by introducing some Skolem functions, and this process is known as skolemization. But according to the definition, it may be impossible to remove existential quantifiers in stable model semantics by such an approach. In this section, we present a translation to eliminate quantifiers in firstorder theories under stable model semantics. We should note that our translation works only for finite structures.

As shown in [Cabalar et al., 2005], there is also a translation that converts every universal theory to a strongly equivalent 3 disjunctive logic program. Combining these two translations, we can then implement a solver for first-order theories which first reduces the input first-order theory to a disjunctive logic program; then invokes a traditional ASP solver that uses the logic program and an extensional database as its input.

Our main idea of quantifier elimination under stable model semantics is intuitively as follows. Suppose ϕ is a formula of the form ∀x∃yϑ(x, y) where ϑ is quantifier-free, and ¯ P a tuple of predicates. Then SM(ϕ; ¯ P) is actually the formula:

To remove ∃y from the formula, we simulate ∀x∃yϑ(x, y) by a formula ∃Sγ and simulate ∀x∃ySt(ϑ(x, y); ¯ P) by a formula ∃XTϱ. Then, by some encoding techniques, we carefully encode γ and ϱ by a universal formula ψ such that ∃S∃TSM(ψ; ¯ P, S, T) is equivalent to SM(ϕ; ¯ P ).

To carry out the simulations mentioned above, we use Eiter et at.'s idea [1996], which is employed to simulate existential quantifier in classical logic. Informally, their idea is as follows. Suppose P is a property on a finite domain D equipped with a linear order. Define S as an auxiliary property on D such that a has property S iff there exists b no less than a such that b has property P . Then if we want to answer the problem whether there is an element with property P, we need only check whether the least element has property S. For more details, please refer to Theorem 2.1 in [Eiter et al., 1996].

The main difficulty in constructing the translation is to find a proper encoding of γ and ϱ. But we have found one. The translation τ is defined as follows. Given a first-order sentence ϕ of the form ∀¯x∃¯ yϑ(¯x, ¯ y), we let τ(ϕ) stand for the conjunction of all sentences which are obtained from the following formulae by applying the universal closure:

where S and T are two predicates of arity |¯x|+|¯ y| and have no occurrence in ϕ, ϑ¬¬(¯x, ¯ y) is obtained from ϑ(¯x, ¯ y) by substituting ¬¬P (¯ t) for all atoms P(¯ t), mın and max denote the

3 Given two arbitrary first-order sentences ϕ and ψ, ϕ is strongly equivalent to ψ if, for any first-order sentence γ and any tuple ¯ P of predicate constants, SM(γ; ¯ P) is equivalent to SM(γ0; ¯ P), where γ0 is obtained from γ by replacing some occurrences of ϕ by ψ.

|¯ y|-tuples (min, . . . ,min) and (max, . . . ,max) respectively, and succ stands for a formula that describes the successor relation on tuples of length |¯ y|. (Clearly, such a formula can be easily built from predicate constant succ.)

Remark 1. In above translation, let us assume that ϕ is a Πksentence for some k ≥ 1. By Theorem 6.4 in [Pearce and Valverde, 2005] and Theorem 8 in [Ferraris et al., 2011], it is not difficult to see that τ(ϕ) can be written as a strongly equivalent Πk-1-sentence. So, every first-order sentence in prenex normal form can be converted to a universal sentence by applying translation τ and the above procedure repeatedly.

The following proposition says that translation τ is faithful.

Proposition 1. Let ϕ be any first-order sentence of the form ∀¯x∃¯ yϑ(¯x, ¯ y) without occurrence of any successor constants. Let ¯ P be any tuple of predicates. Then, over successor structures, ∃S∃TSM(τ(ϕ); ¯ P, S, T) is equivalent to SM(ϕ; ¯ P ), where S and T are the auxiliary predicates introduced by τ .

Proof. Let σ be the vocabulary consisting of all constants occurring in ϕ and of all successor constants. Let ̂ σ be the vocabulary of τ(ϕ). Let k = |¯x| and l = |¯ y|. Given any σstructure A, define R(A) as a (k + l)-ary relation on A such that: for all tuples ¯a ∈ Ak and ¯b ∈ Al , (¯a, ¯b) ∈ R(A) iff there is a tuple ¯ c ≥ ¯b (wrt the successor relation) such that ϑ(¯a, ¯ c) is satisfied by A; for each tuple ¯a ∈ Ak , let ℑ(A, ¯a) denote the largest one of all tuples ¯b ∈ Al such that (¯a, ¯b) ∈ R(A).

We first assume that A is a finite successor σ-structure that satisfies SM(ϕ; ¯ P). Let B be a ̂ σ-expansion of A that interprets S as the relation R(A) and T as the relation Ak+l . Then we want to show that B satisfies SM(τ(ϕ); ¯ P, S, T). It is not difficult to check B satisfies τ(ϕ). Let β be any assignment in B that satisfies ¯X¯ PST < ¯ PST . To obtain a contradiction, assume that β satisfies St(τ(ϕ); ¯ P, S, T). Note that the formula ∀¯x¯ y¯ zSt((3); ¯ P, S, T) is clearly a logical consequence of the formula St(τ(ϕ); ¯ P , S, T ) in classical first-order logic, and β satisfies the former in B iff β satisfies the formula

in B. So we must have that β(XS) = B(S), and this implies that ¯X¯ P < ¯ P should be satisfied by β. Otherwise, for all tuples ¯a ∈ Ak , St(ϑ(¯a,ℑ(A, ¯a)); ¯ P) has the same truth with ϑ(¯a,ℑ(A, ¯a)) (and so is true) in β. Consequently (¯a, A(max)) belongs to β(XT ) since the universal closure of

should be satisfied by β in B (Note that St(τ(ϕ); ¯ P, S, T) is satisfied by β in B by the assumption). Since the formula

is clearly satisfied by β in B, the above conclusion leads to β(XT ) = B(T), a contradiction. Therefore, we have that β satisfies ¯X¯ P < ¯ P . Let α denote the assignment in A obtained by restricting β to variables in ¯X¯ P . Clearly, α satisfies ¯X¯ P < ¯ P in A. On the other hand, as β satisfies St(τ(ϕ); ¯ P , S, T ), for each tuple ¯a ∈ Ak , one of the following cases should be true: (i) St(ϑ(¯a,ℑ(A, ¯a)); ¯ P , S, T ) is satisfied by β in B; (ii)

there is at least one tuple ¯b ∈ Al such that St(ϑ(¯a, ¯b); ¯ P , S, T ) is satisfies by β in B. In either case, we have that β satisfies St(∃¯ yϑ(¯a, ¯ y); ¯ P , S, T ) in B, which will imply that α satisfies St(∀¯x∃¯ yϑ(¯x, ¯ y); ¯ P) in A. But this is impossible since, by the assumption, A is a model of SM(ϕ; ¯ P ).

Conversely, let us assume that B is a ̂ σ-structure that satisfies SM(τ(ϕ); ¯ P , S, T ). Let A be the restriction of B to σ. Now our task is to show A is a model of SM(ϕ; ¯ P). Since B satisfies the universal closure of formula (3), it is true that B(S) ⊇ R(A). Moreover, we can show that B(S) equals to R(A). Otherwise, there is an assignment β in B such that: (i) β(XS) = R(A) and β(XT ) = Ak+l , and (ii) β satisfies both ¯X¯ PST < ¯ PST and St(τ(ϕ); ¯ P, S, T) in B. Obviously, these contradicts with the assumption. Note also that formula ∀¯x(2) is clearly satisfied by B. So, for each tuple ¯a ∈ Ak , it must hold that B(S) contains (¯a,B(mın)), or equivalently, (¯a,B(mın)) ∈ R(A). By the definition, there should exist at least one tuple ¯ c ∈ Al such that ϑ(¯a, ¯ c) is true in A. Immediately, we can obtain that ϕ is satisfied by A.

Let α be any assignment in A that satisfies ¯X < ¯ P. To complete the proof, we need show that St(ϕ; ¯ P) is unsatisfied by α in A. To obtain a contradiction, assume this is not true. Let β be an assignment in B such that: (i) for all P in ¯ P , β(XP ) equals to α(XP ); (ii) β(XS) = R(A); and (iii) for all ¯a ∈ Ak and all ¯b ∈ Al , (¯a, ¯b) ∈ β(XT ) iff (¯a, ℑ(A, ¯a)) ∈ R(A) or there is some tuple ¯ c > ¯b such that St(ϕ(¯a, ¯ c); ¯ P ) is satisfied by α in A. Then it is not difficult to verify that β satisfies St(τ(ϕ); ¯ P, S, T). Note that ¯X¯ PST < ¯ PST is clearly satisfied by β. So the conclusion will imply that B is not a model of SM(τ(ϕ); ¯ P , S, T ), a contradiction.

According to Corollary 6.5 in [Pearce and Valverde, 2005] and Theorem 8 in [Ferraris et al., 2011], under stable model semantics, there exist some translations which convert every first-order sentence into a strongly equivalent sentence in prenex normal form. Let τ0 be one of those which translate τ(ϕ) into a Πk-1-sentence for all integers k ≥ 1 and all Πksentences ϕ. Let τ ∗ be a translation that applies τ0 and τ repeatedly until the resulting sentence is universal. So, by Proposition 1 and Remark 1, we have the faithfulness of τ ∗ :

Theorem 1. Let ϕ be any first-order sentence that has no occurrence of any successor constants. Let ¯ P be any tuple of predicates. Then ∃ ¯QSM(τ ∗ (ϕ); ¯ P, ¯Q) is equivalent to SM(ϕ; ¯ P) over finite successor structures, where ¯Q is the tuple of auxiliary predicates introduced by τ ∗ .

In fact, this theorem can be generalized to finite structures.

Corollary 1. For every first-order sentence ϕ, there are a universal first-order sentence ψ and a tuple ¯Q of new predicates such that ∃ ¯QSM(ψ; ¯ P, ¯Q) is equivalent to SM(ϕ; ¯ P ) over finite structures for all tuples ¯ P of predicate constants.

Proof. (Sketch) Given a first-order sentence ϕ, let ϖ be a first-order sentence asserting that a finite σ-structure A satisfies ∃ ¯OSM(ϖ; ¯O) iff A is a successor structure, 4 where σ = {succ,min,max} and ¯O is the tuple of all predicate constants which occur in ϖ and which have no occurrences in both ϕ and σ. Let ψ = ϖ ∧ τ ∗ (ϕ), and let ¯ P be any tuple of predicate constants. By Theorem 1, there is a tuple ¯Q of auxiliary predicates such that SM(ϕ; ¯ P) is equivalent to ∃ ¯QSM(τ ∗ (ϕ); ¯ P, ¯Q). Also by Splitting Lemma in [Ferraris et al., 2009], SM(ψ; ¯O, ¯ P, ¯Q) is equivalent to the formula SM(ψ; ¯O) ∧ SM(ψ; ¯ P, ¯Q). By the definition, the latter is equivalent to the formula SM(ϖ; ¯O) ∧ SM(τ ∗ (ϕ); ¯ P, ¯Q). Then, it is not difficult to verify that SM(ϕ; ¯ P) is equivalent to ∃ ¯O∃ ¯QSM(ψ; ¯O, ¯ P, ¯Q) over finite structures.

4 One can find such a sentence in [Eiter et al., 1997].

Remark 2. As seen in the above corollary, it is not necessary to equip any structure with a successor relation. Notice that almost all traditional ASP solvers (e.g., CLASP, DLV, etc.) support a set of built-in arithmetic functions or predicates which can be used to define the successor relation. Therefore, when we implement a solver for first-order theories, it is enough to consider a translation over successor structures.

Remark 3. An exponential growth in the formula size seems inevitable in the worst case when we convert a universal sentence to a strongly equivalent logic program. It is because we have to apply rules like "distributive law" frequently (cf. [Cabalar et al., 2005]). The situation will slightly improve for a theory since we can directly apply Cabalar et al.'s translation to each sentence in the theory. So we should make each sentence in resulting theory of quantifier elimination as short as possible. τ ∗ is not good for this purpose. But fortunately, we can improve it by the following property, which can be obtained by a slight modification of the proof for Proposition 1.

Proposition 2. Let ϕ and ψ be any first-order sentences without occurrences of successor constants, and in particular ϕ is of the form ∀¯x∃¯ yϑ(¯x, ¯ y). Let ¯ P be any tuple of predicates. Then, over successor structures, SM(ϕ∧ψ; ¯ P) is equivalent to ∃S∃TSM(τ(ϕ)∧ψ; ¯ P , S, T ), where S and T are auxiliary predicates introduced by τ and have no occurrences in ψ.

Having this proposition, we can directly apply τ to each conjunct of the input formula. Based on this idea, we then devise a new translation τ ⋄ which works as follows. For every first-order sentence ϕ, translation τ ⋄ repeatedly do stages 1-3 until the resulting formula is universal already:

1. Lift the conjunctions in ϕ as many as possible. For instance, (ψ∧ϱ)∨γ will be converted to (ψ∨γ)∧(ϱ∨γ).
2. Convert each conjunct of the result of stage 1 to a formula in prenex normal form.
3. Apply τ to each conjunct of the result of stage 2.

Due to the space limit, we simply illustrate it by an example. Example 1. Let ϕ = ∃x∀yθ(x, y) be a sentence, where θ(x, y) is a quantifier-free formula to which stage 1 cannot be applied anymore. Then, on input ϕ, τ ⋄ will do stages 1-3 twice. In the first round, ϕ will not change at stages 1-2, but after stage 3 we will obtain the following theory:

In the second round, we only explain how the translation τ ⋄ works on sentence (8). After stage 1, we will obtain:

And we will have (12) and ∀x∃y(謬(x, y) → S1(x)) after stage 2. Furthermore, the resulting theory of stage 3 will consist of (12) and the following sentences:

where λ(x, y) stands for the formula 謬(x, y) → ¬¬S1(x) and η(x, y) for the formula 謬(x, y) → S1(x).

Remark 4. As seen in the above example, each sentence in the resulting theory is of size 5 O(k+n), where k is the number of quantifier alternating blocks in the original theory and n the maximum size of conjuncts in the original theory. Since k is usually very small, this improvement assures the resulting logic program of the reduction will be of a reasonable size.

With the above results, a natural problem may be: is there a translation that does not use auxiliary predicates? The following theorem asserts the nonexistence of such a translation even if we only consider the case of finite structures.

Theorem 2. Over finite structures, there exists a first-order sentence ϕ involving only one binary predicate constant R such that, for any universal first-order sentence ψ of the same vocabulary, SM(ϕ;R) is not equivalent to SM(ψ;R).

Proof. (Sketch) Let σ be a vocabulary consisting of a binary predicate constant R. Let ODD∗ be the class of finite σ-structures A such that: (i) |A| is odd or equals to 2, and (ii) A(R) = A2 . Let ζ be the conjunction of following sentences:

Let ξ be the sentence ∀w∀w′ (¬¬R(w, w′ )∧(R(w, w′ )∨ζ)). Then we can show that SM(ξ; R) encodes exactly ODD∗ , i.e., a finite σ-structure A is an R-stable model of ξ iff A ∈ ODD∗ .

On the other hand, we can show there is no universal firstorder σ-sentence ψ such that ODD∗ is exactly the class of finite R-stable models of ψ. Since for every universal firstorder σ-sentence ψ, SM(ψ;R) can be written as a secondorder sentence of the form ∀ ¯X∀¯x∃¯ yϑ, where ¯X is a tuple of predicate variables, ¯x, ¯ y two tuples of individual variables, and ϑ a quantifier-free formula. By a slight modification to the proof for Theorem 2.2 of [Eiter et al., 1996], we can show that ODD∗ cannot be defined by any of such sentences.

5 We count the occurrences of quantifiers, connectives and atoms.

4 FromCircumscription to Stable Models

According to Lin's transformation (cf. [Lin and Zhou, 2011]), stable model semantics can be translated to circumscription in some sense. In this section, we give a translation that embeds circumscription into stable model semantics. Surprisingly, it does not involve any auxiliary predicates, and works for arbitrary structures. Together with the reduction in previous section, we can then translate first-order theories of circumscription into logic programs under stable model semantics.

Let ϕ be a first-order sentence, and ¯ P a tuple of predicates. Clearly, ϕ can be converted to a sentence ̂ ϕ in negational normal form without implication (i.e, a formula built from literals by ∧, ∨, ∀ and ∃). 6 Then, we define the translation π ¯ P as a mapping that maps each first-order formula ϕ to the formula

where ̂ ϕ¬¬ is same as in the previous section, and ˜ ϕ obtained from ̂ ϕ by substituting P(¯ t) → ∧R∈ ¯ P ∀¯u (R(¯u) ∨ ¬R(¯u)) (denoted by P ∼(¯ t)) for each literal ¬P(¯ t) such that P ∈ ¯ P .

Theorem3. CIRC(ϕ; ¯ P) is equivalent to SM(π ¯ P (ϕ); ¯ P) for any first-order sentence ϕ and any tuple ¯ P of predicates.

Proof. Clearly, we have that CIRC(ϕ; ¯ P) is equivalent to CIRC( ̂ ϕ; ¯ P). By definition, CIRC(̂ ϕ; ¯ P) is exactly the sentence ̂ ϕ ∧ ∀ ¯X ¯ P ( ¯X¯ P < ¯ P → ¬ ̂ ϕ( ¯X¯ P )) and SM(π ¯ P (ϕ); ¯ P ) is the sentence π ¯ P (ϕ) ∧ ∀ ¯X ¯ P ( ¯X¯ P < ¯ P → ¬St(π ¯ P (ϕ); ¯ P )). By a routine simplification, the latter is equivalent to

where δ denotes ∧R∈ ¯ P ∀¯u(XR(¯u) ∨¬R(¯u)). Let σ be the vocabulary of ϕ, and let A be a σ-structure and α an assignment in A that satisfies ¯X¯ P < ¯ P. It is easy to see that δ is always false in α. As ̂ ϕ is in negational normal form without implication, it is not difficult to see that α satisfies St(˜ ϕ; ¯ P ) iff α satisfies ̂ ϕ( ¯X¯ P ) (Notice that α satisfies St(P ∼(¯ t); ¯ P ) iff α satisfies ¬XP (¯ t) since δ is false in α). So we can conclude that formula (24) is equivalent to CIRC(̂ ϕ; ¯ P), which completes the proof immediately.

As we have seen in the definition of circumscription, no varying predicates are considered. For some applications of circumscription (e.g., model update), however, varying predicates may be important. In this case, we should firstly use the translation given in [Cadoli et al., 1992] to eliminate varying predicates, and then transform the result to a logic program.

5 Benchmarks and Experiments

Based on the translation approach described earlier, we have implemented a prototype solver T2LP for first-order ASP. The input of our solver contains an arbitrary first-order theory and a class of finite extensional databases. The solver firstly "compiles" (so only once) the theory to a logic program, and then computes stable models by invoking a traditional ASP solver on the logic program and on each extensional database.

6 By the definition, the equivalence between formulae in classical first-order logic implies that in circumscription. So, it suffices to find such a translation in classical first-order logic, which clearly exists.

Two benchmarks are used to test T2LP. The first one is the clique coloring problem and the second one the quantified boolean satisfiability problem. Both benchmarks can be easily encoded in first-order theories with existential quantifiers. To the best of our knowledge, no natural encodings in disjunctive logic programs are available for these problems.

5.1 Clique Coloring Problem

The problem of clique coloring is Σp2 -complete and has been thoroughly studied in graph theory. Here we consider only the version of 2-color that still remains Σp2 -complete (cf. [Schaefer and Umans, 2002]). The problem is defined as follows. Given a graph G = (V, E), does G have a 2-clique-coloring? Herein, a 2-clique-coloring is a function from V to {0, 1} such that each maximal clique of G contains two vertices of different colors. Let Γ denote the following first-order theory:

where the vocabulary of Γ consists of unary predicate constants col, col, set, set, of a binary predicate constant edg, of a nullary predicate constant ok. Let ¯ P denote the tuple of above predicate constants of arity less than 2. Every graph G = (V, E) is encoded to be a {edg}-structure AG such that the domain is V and edg is interpreted as E. By a reason similar to that in Examples 2 of [Eiter et al., 1997], AG is a model of ∃ ¯ PSM(Γ; ¯ P) iff G has a 2-clique-coloring.

5.2 QBF Satisfiability Problem

It is well-known that the following problem is Σp2 -complete: Given a quantified boolean formula ∀¯ pϕ where ¯ p is a tuple of propositional variables and ϕ is quantifier-free and in disjunctive normal form, is the formula satisfiable? To show our solver works well for theories with more quantifier alternations, we modify the original problem by allowing ϕ to be a conjunction of a CNF-formula and a DNF-formula. Clearly, the new problem remains Σp2 -complete. Let tr, tr and un be unary predicate constants, let pc, nc, pd and nd be binary predicate constants, and let ok be a nullary predicate constant. Then Δ is defined as the following first-order theory:

Let σ denote the set of predicate constants un, pc, nc, pd, nd. For every input, i.e., a formula ∀¯ pϕ of the form mentioned previously, we can construct a σ-structure A to encode it in the following way: (i) the domain A of A is the integer set Zn = {0, . . . , n - 1}, where n is the largest of the number of clauses of the CNF-formula, the number of clauses of the DNF-formula, and the number of propositional variables occurring in ϕ; (ii) (i, k) ∈ A(pc) ((i, k) ∈ A(nc)) if the k-th variable has a positive (negative) occurrence in the i-th clause of the CNF-formula; (iii) (i, k) ∈ A(pd) ((i, k) ∈ A(nd)) if the k-th variable has a positive (negative) occurrence in the i-th clause of the DNF-formula; (iv) i ∈ A(un) iff pi ∈ ¯ p. Similarly, it is easy to show that A satisfies ∃tr∃tr∃okSM(Δ; σ, tr, tr, ok) iff ∀¯ pϕ is satisfiable.

5.3 Experimental Results

Experimental results for these two benchmarks are presented in Tables 1 and 2 respectively. The parameter n in Table 1 (Table 2) denotes the number of vertices in the graph G (the number of propositional variables in the formula ϕ). Each instance for either experiment is randomly generated. In particular, in the experiment of QBF satisfiability, both the number of CNF clauses and the number of DNF clauses equals to n. Non-integer real numbers in the tables figure the run time (in seconds) of the solver to compute the first stable model. If the time exceeds one hour, we simply write it as "> 1h" in the table. All experiments were run on a 2.7GHz PC on Linux.

As we can see in the tables, each instance of each benchmark is computed twice by our translation calling different ASP solvers: CLASPD and DLV. In general, the solver using CLASPD is faster than that using DLV. Though our translation is of general purpose and both benchmarks are Σp2 - complete, the experimental results seem quite optimistic.

6 Conclusion and RelatedWork

In this paper, we proposed an approach to reduce first-order theories to logic programs under stable model semantics over finite structures. The effectiveness of our approach was demonstrated by both theoretical analysis and experiments. We also discovered an embedding of circumscription into stable model semantics. These results provide useful insights for developing practical solvers for arbitrary first-order theories under either stable model semantics or circumscription.

Two different translations from first-order theories to logic programs were presented in [Kim et al., 2009; Lee and Palla, 2009] and [Cabalar, 2009] respectively. However, their translations only work on some fragments, and it is not clear how their work can be soundly extended to the general case (or fragments that contain the benchmarks in this paper). In addition, even restricted to those fragments, our translation is significantly different from theirs. Also, the translation from circumscription to logic programs was considered by Janhunen and Oikarinen [2004] in the propositional case, which, in our opinion, seems not easy to be extended to the first-order case.