We develop a formal framework intended as a preliminary step for a single knowledge representation system that provides different representation techniques in a unified way. In particular we consider first-order logic extended by techniques for second-order quantifier elimination and non-monotonic reasoning. Background of the work is literal projection, a generalization of second-order quantification which permits, so to speak, to quantify upon an arbitrary sets of ground literals, instead of just (all ground literals with) a given predicate symbol. In this paper, an operator raise is introduced that is only slightly different from literal projection and can be used to define a generalization of circumscription in a straightforward and compact way. Some properties of this operator and of circumscription defined in terms of it, also in combination with literal projection, are then shown. A previously known characterization of consequences of circumscribed formulas in terms of literal projection is generalized from propositional to first-order logic. A characterization of answer sets according to the stable model semantics in terms of circumscription is given. This characterization does not recur onto syntactic notions like reduct and fixed-point construction. It essentially renders a recently proposed “circumscription-like” characterization in a compact way without involvement of a specially interpreted connective.
We develop a formal framework intended as a preliminary step for a single knowledge representation system that provides different representation techniques in a unified way. In particular we consider first-order logic extended by techniques for second-order quantifier elimination and non-monotonic reasoning.
Second-order quantifier elimination permits to express a large number of
knowledge representation techniques (see for example [
We focus here on a particular generalization of second-order quantifier
elimination, the computation of literal projection [
In particular, we consider circumscription and, based on it, the stable model
semantics, which underlies many successful applications developed during the
last decade. It is well-known that the processing of circumscription can be
expressed as a second-order quantifier elimination task [
The paper is structured as follows: Preliminaries are given in Section 2, including
a description of the used semantic framework and a summary of background
material on literal projection. In Sections 3–7 the proper contributions of this
paper are described and formally stated. Proofs of propositions and theorems
as well as more details on the relationship of the introduced definition of stable
models to other characterizations can be found in the extended report version
of this paper [
Symbols. We use the following symbols, also with sub- and superscripts, to stand for items of types as indicated in the following table (precise definitions of these types are given later on in this section). They are considered implicitly as universally quantified in definition, theorem and proposition statements.
F, G – Formula
A – Atom L – Literal S – Set of ground literals (also called literal scope)
M – Consistent set of ground literals I, J, K – Structure
β – Variable assignment Notation. Unless specially noted, we assume that a first-order formula is constructed from first-order literals, truth value constants ⊤, ⊥, the unary connective ¬, binary connectives ∧, ∨ and the first-order quantifiers ∀ and ∃. We write the positive (negative) literal with atom A as +A (−A). Variables are x, y, z, also with subscripts. As meta-level notation with respect to this syntax we use implication →, biconditional ↔ and n-ary versions of the binary connectives.
A clause is a sentence of the form ∀x1 . . . ∀xn(L1 ∨ . . . ∨ Lm), where n, m ≥ 0 and the Li for i ∈ {1, . . . , m} are literals. Since all variables in a clause are universally quantified, we sometimes do not write its quantifier prefix.
We assume a fixed first-order signature with at least one constant symbol. The sets of all ground terms and all ground literals, with respect to this signature, are denoted by TERMS and ALL, respectively.
The Projection Operator and Literal Scopes. A formula in general is like
a first-order formula, but in its construction two further operators, project(F, S)
and raise(F, S), are permitted, where F is a formula and S specifies a set of
ground literals. We call a set of ground literals in the role as argument to project
or raise a literal scope. We do not define here a concrete syntax for specifying
literal scopes and just speak of a literal scope, referring to the actual literal
scope in a semantic context as well as some expression that denotes it in a
syntactic context. The formula project(F, S) is called the literal projection of F
onto S. Literal projection generalizes existential second-order quantification [
Interpretations. We use the notational variant of the framework of Herbrand
interpretations described in [
lation between interpretations I = hI, βi and formulas is defined by the clauses in Tab. 1, where L matches a literal, F, F1, F2 match a formula, and S matches a literal scope. In the table, two operations on variable assignments β are used: If F is a formula, then F β denotes F with all variables replaced by their image in β; If x is a variable and t a ground term, then β xt is the variable assignment that maps x to t and all other variables to the same values as β. Entailment and equivalence are straightforwardly defined in terms of the satisfaction relation. Entailment: F1 |= F2 holds if and only if for all hI, βi such that hI, βi |= F1 it holds that hI, βi |= F2. Equivalence: F1 ≡ F2 if and only if F1 |= F2 and F2 |= F1.
Intuitively, the literal projection of a formula F onto scope S is a formula
that expresses about literals in S the same as F , but expresses nothing about
other literals. The projection is equivalent to a formula without the projection
operator, in negation normal form, where all ground instances of literals
occurring in it are members of the projection scope. The semantic definition of literal
projection in Tab. 1 can be alternatively expressed as: An interpretation hI, βi
satisfies project(F, S) if and only if there is a structure J such that hJ, βi
satisfies F and I can be obtained from J by replacing literals that are not in S with
their complements. This includes the special case I = J , where no literals are
replaced.
Relation to Conventional Model Theory. Literal sets as components of
interpretations permit the straightforward definition of the semantics of literal
projection given in the last clause in Tab. 1. The set of literals I of an
interpretation hI, βi is called “structure”, since it can be considered as
representation of a structure in the conventional sense used in model theory: The
domain is the set of ground terms. Function symbols f with arity n ≥ 0 are
mapped to functions f ′ such that for all ground terms t1, ..., tn it holds that
f ′(t1, ..., tn) = f (t1, ..., tn). Predicate symbols p with arity n ≥ 0 are mapped to
{ht1, ..., tni | +p(t1, ..., tn) ∈ I}. Moreover, an interpretation hI, βi represents a
conventional second-order interpretation [
formula F in negation normal form is the set of all ground instances of literals in F . The following formal definition generalizes this notion straightforwardly for formulas that are not in negation normal form and possibly include the project and raise operator: L(L) is the set of all ground instances of L; ] L(⊤) d=ef L(⊥) d=ef {}; L(¬F ) d=ef L(F ); L(F ⊗ G) d=ef L(F ) ∪ L(G) if ⊗ is ∧ or ∨; L(⊗xF ) d=ef L(⊗(F, S)) d=ef L(F ) if ⊗ is a quantifier or the project or raise operator, respectively.
We call the set of ground literals “about which a formula expresses
something” its essential literal base, made precise in Def. 1 (see [
mula F, in symbols LE (F ), is defined as LE (F ) d=ef {L | L ∈ ALL and there exists
an interpretation hI, βi such that hI, βi |= F and hI[Le], βi 6|= F }.
Properties of Literal Projection. A summary of properties of literal
projection is displayed in Tab. 2 and 3. Most of them follow straightforwardly from
the semantic definition of project shown in Tab. 1 [
The following operator raise is only slightly different from literal projection and, as we will see later on, can be used to define a generalization of parallel circumscription with varied predicates in a straightforward and compact way. Definition 3 (Raise).
hI, βi |= raise(F, S) iffdef there exists a J such that hJ, βi |= F and J ∩ S ⊂ I ∩ S.
The definition of raise is identical to that of literal projection (Tab. 1), with the exception that J ∩ S and I ∩ S are related by the proper subset instead of the subset relationship.
The name “raise” suggests that a model hI, βi of raise(F, S) is not “the lowest” model of F , in the sense that there exists another model hJ, βi of F with the property J ∩ S ⊂ I ∩ S. An equivalent specification of the condition J ∩ S ⊂ I ∩ S in the definition of raise provides further intuition on its effect: A literal scope S can be partitioned into three disjoint subsets Sp, Sn, Spn such that Sp (Sn) is the set of positive (negative) literals in S whose complement is not in S, and Spn is the set of literals in S whose complement is also in S. Within Def. 3, the condition J ∩ S ⊂ I ∩ S can then be equivalently expressed by the conjunction of J ∩ (Sp ∪ Sn) ⊂ I ∩ (Sp ∪ Sn) and J ∩ Spn = I ∩ Spn. That is, with respect to members of S whose complement is not in S, the structure J must be a proper subset of I, and with respect to the other members of S it must be identical to I.
Proposition 1 below shows some properties of the raise operator: It is
monotonic (Prop. 1.i). From this follows that it is a “semantic” operator in the sense
that for equivalent arguments the values are equivalent too (Prop. 1.ii). Like
projection, the raise operator distributes over disjunction (Prop. 1.iii).
Proposition 1.iv follows from monotonicity. Proposition 1.v shows that for scopes that
contain exactly the same atoms positively as well as negatively, raise is
inconsistent. Propositions 1.vi and 1.vi show the interplay of raise with projection onto
the same scope. Proposition 1.viii provides a characterization of literal
projection in terms of raise and atom projection [
(i) If F1 |= F2, then raise(F1, S) |= raise(F2, S). (ii) If F1 ≡ F2, then raise(F1, S) ≡ raise(F2, S). (iii) raise(F1 ∨ F2, S) ≡ raise(F1, S) ∨ raise(F2, S). (iv) raise(F1 ∧ F2, S) |= raise(F1, S) ∧ raise(F2, S). (v) If S = Se, then raise(F, S) ≡ ⊥. (vi) raise(project(F, S), S) ≡ raise(F, S). (vii) project(raise(F, S), S) ≡ raise(F, S). (viii) project(F, S) ≡ project(F, S ∪ Se) ∨ raise(F, S).
The following definition specifies a formula circ(F, S) that provides a characterization of circumscription in terms of raise, as we will first outline informally and then show more precisely.
circ(F, S) d=ef F ∧ ¬raise(F, S).
In this notation, the parallel circumscription of predicate constants P in
sentence F with varied predicate constants Z [
In other words, the scope S contains the circumscribed predicates just positively (the positive literals according to item 1.), and the “fixed” predicates in full (all positive as well as negative literals according to item 2.). Since the literal scope in circ(F, S) can be an arbitrary sets of literals, circ(F, S) is more general than parallel circumscription with varied predicates: Model maximization conditions can be expressed by means of scopes that contain negative literals but not their complements. Furthermore, it is possible to express minimization, maximization and variation conditions that apply only to a subset of the instances of a predicate.
We now make precise how circ relates to the established definition of
circumscription by means of second-order quantification [
i=1 i=1 Considering the predicate symbols in P ′ and Z′ as predicate variables, the second-order circumscription of P in F with variable Z, written CIRC[F ; P ; Z], is then defined as:
CIRC[F ; P ; Z] d=ef F ∧ ¬∃P ′, Z′ (F ′ ∧ P ′< P ). Existential second-order quantification can be straightforwardly expressed with literal projection: ∃p G corresponds to project(G, S), where S is the set of all ground literals with a predicate other than p. From Tab. 2.xv it can be derived that also a smaller projection scope is sufficient: project(G, S) is equivalent to project(G, S′) for all subsets S′ of S that contain those literals of S whose predicate symbol occurs in G. Accordingly, CIRC[F ; P ; Z] can be expressed straightforwardly in terms of literal projection instead of the second-order quantification:
Let F be a first-order formula and let P, P ′, Z, Z′ be tuples of predicate symbols as specified in the definition of CIRC (Def. 5). Let Q be the set of predicate symbols in F that are neither in P nor in Z. Then CIRC-PROJ[F ; P ; Z] is a formula with the projection operator, defined as:
CIRC-PROJ[F ; P ; Z] d=ef F ∧ ¬project(F ′ ∧ P ′< P, Pˆ ∪ Qˆ).
The Q parameter in Def. 6 is the set of the “fixed” predicates. The set of literals (Pˆ ∪ Qˆ) suffices as projection scope, since the quantified body of the right conjunct of CIRC[F ; P ; Z], that is, (F ′ ∧P ′< P ), contains – aside of the quantified predicate symbols from P ′, Z′ – just predicate symbols that are in P or in Q.
The following theorem makes precise how second-order circumscription can
be expressed with circ. Its proof in [
Theorem 1 (Second-Order Circumscription Expressed by circ). Let F be a first-order formula and let P, P ′, Z, Z′ be tuples of predicate symbols as specified in the definition of CIRC (Def. 5). Let Q be the set of predicate symbols in F that are neither in P nor in Z. Then
CIRC-PROJ[F ; P ; Z] ≡ circ(F, (Pˆ ∩ POS) ∪ Qˆ). 5
As discussed in [
to S if and only if
F |= project(circ(F, S), S).
In this definition, the literal scope S can be an arbitrary set of literals,
corresponding to variants of circumscription as indicated in Sect. 4. We now explicate
how this definition renders the definition of well-foundedness in [
The following proposition shows properties of projection nested within circumscription. It is independent of the well-founded property.
(i) circ(F, S) |= circ(project(F, S), S).
(ii) circ(project(F, S), S) |= circ(project(F, S ∪ Se), S).
In the special case where S ∪ Se = ALL, which holds for example if S = POS, the two entailments Prop. 2.i and Prop. 2.ii can be combined to the equivalence circ(project(F, S), S) ≡ circ(F, S). From this equivalence, it can be derived that two formulas which express the same about positive literals (that is, have equivalent projections onto POS) have the same minimal models (that is, have equivalent circumscriptions for scope POS).
The following proposition concerns circumscription nested within projection. It is a straightforward consequence of the definition of well-founded along with Tab. 2.vi and 2.ii.
respect to S, then
project(circ(F, S), S) ≡ project(F, S).
From this proposition follows that if two well-founded formulas have equivalent
circumscriptions for some scope, then also their projections onto that scope are
equivalent. With properties of projection, it also follows that if S is a positive
literal scope (that is, S ⊆ POS) then project(circ(F, POS), S) ≡ project(F, S). This
equivalence can be applied to provide a straightforward justification for applying
methods to compute minimal models also to projection computation onto
positive scopes: We consider methods that compute for a given input formula F an
output formula F ′ that satisfies syntactic criteria (for example correspondence to
a tableau) which permit projection computation with low computational effort,
such that projection computation is in essence already performed by
computing F ′. Assume that the output formula has the same minimal models as the
input formula, that is, circ(F ′, POS) ≡ circ(F, POS). If F ′ is well-founded, for
positive literal scopes S it then follows that project(F ′, S) ≡ project(F, S). A
tableau constructed by the hyper tableau calculus can indeed be viewed as
representation of such a formula F ′ [
Literal forgetting is a variant of literal projection that can be defined as
forget(F, S) d=ef project(F, S) and is investigated for propositional logic in [
These characterizations are rendered here in terms of literal projection as
Theorem 2.ii and 2.iii below, where we generalize and make more precise the
statements given in [
This basic variant is actually a straightforward generalization of
Proposition 12 in [
circ(F, S) |= G is equivalent to (at least) one of the following statements, depending on LE (G): (i) F |= G, (ii) F |= project(F ∧ G, S), (iii) F |= project(F ∧ ¬project(F ∧ ¬G, S), S). if LE (G) ⊆ S; if LE (G) ⊆ (S ∪ Se); 7
In [
We let the symbols ◦ and • denote these predicates. They are unary, and we write them without parentheses – for example •p(a). With them, we now formally define a notion of logic program. Its correspondence to the more conventional view of a logic program as formed by non-classical operators will then be indicated.
Definition 8 (Logic Program).
(i) A rule clause is a clause2 of the form m n o p _−◦Ai ∨ _+•Bi ∨ _+◦Ci ∨ _−•Di, i=1 i=1 i=1 i=1 where k, m, n, o, p ≥ 0 and the subscripted A, B, C, D are terms.
(ii) For a rule clause of the form specified in (8.i), the rule clause (Wim=1−◦Ai ∨ Win=1+•Bi) is called its negated body, and the rule clause (Wio=1+◦Ci∨Wip=1−•Di) is called its head.
(iii) A logic program is a conjunction of rule clauses.
(iv) The symbol SYNC stands for the formula ∀x(+•x ↔ +◦x). Conventionally, logic programs are typically notated by means of a special syntax with truth value constants (⊤, ⊥), conjunction (,), disjunction (;), negation as failure (not) and rule forming (→) as connectives. A rule clause according to (Def. 8.i) is then written as a rule of the form
A1, . . . , Am, not B1, . . . , not Bn → C1; . . . ; Co; not D1; . . . ; not Dp, (i) where m, n, o, p ≥ 0 and the subscripted A, B, C, D are atoms. If m = n = 0, then the left side of the rule is ⊤; if o = p = 0, then the right side is ⊥. 2 Recall that a clause as specified in Sect. 2 may contain universally quantified variables. The implicit quantifier prefixes of clauses are not written in this definition.
The following definition specifies a formula ans(F ) whose models are exactly those interpretations that represent an answer set of F according to the stable model semantics.
ans(F ) d=ef circ(F, POS ∪ •ˆ) ∧ SYNC.
In the definition of ans(F ), the scope of the circumscription, (POS ∪ •ˆ), is equal to ((◦ˆ ∩ POS) ∪ •ˆ) which matches the right side of Theorem 1, indicating that ans(F ) can also be expressed in terms of second-order circumscription.
We now explicate the relationship of the characterization of stable models
by ans(F ) to the characterization in [
Let F be a logic program. Let P = p1, . . . , pn be the function symbols of the principal terms in F (that is, the predicate symbols if the wrapper predicates ◦ and • are dropped). Let P ′ = p′1, . . . , p′n and Q = q1, . . . , qn be tuples of distinct predicate symbols which are disjoint with each other and with P . We use the following notation to express variants of F that are obtained by replacing predicate symbols: – We write F also as F [◦, •], to indicate that ◦ and • occur in it. – The formula F [U, V ], where U = u1, . . . , un and V = v1, . . . , vn are tuples of predicate symbols is F [◦, •] with all atoms ◦(pi(t)) replaced by ui(t) and all atoms •(pi(t)) replaced by ui(t), where t matches the respective argument terms. As a special case, F [P, P ] is then F [◦, •] with all atoms of the form ◦A or •A replaced by A.
Let cnv(F ) denote F converted into the syntax of logic programs with
nonclassical operators used by [
SM(cnv(F )) ≡ F [P, P ] ∧ ¬∃P ′(F [P ′, P ] ∧ P ′< P ).
The right side of equivalence (ii) is not a second-order circumscription, since P occurs in F [P ′, P ] as well as in P ′< P . To fit it into the circumscription scheme, we replace the occurrences of P in F [P ′, P ] by Q and add the requirement that P and Q are equivalent: Let (P ↔ Q) stand for Vn i=1(pi(xi) ↔ qi(xi)), where xi has the same meaning as in Def. 5. The following equivalences then hold:
SM(cnv(F )) ∧ (P ↔ Q) ≡ F [P, Q] ∧ ¬∃P ′(F [P ′, Q] ∧ P ′< P ) ∧ (P ↔ Q) ≡ CIRC[F [P, Q]; P ; ∅] ∧ (P ↔ Q). To get rid of the biconditionals (P ↔ Q) in (iii), projection can be employed: From SM(cnv(F )) ≡ project(SM(cnv(F )) ∧ (P ↔ Q), Pˆ) it follows that SM(cnv(F )) ≡ project(CIRC[F [P, Q]; P ; ∅] ∧ (P ↔ Q), Pˆ). (vi) Based on equivalence (vi), the correspondence of ans(F ) to SM(cnv(F )) can be shown by proving that for two interpretations that are related in a certain way the one is a model of SM(cnv(F )) if and only if the other is a model of ans(F ): Let I be a structure over P and Q as predicate symbols. Define I′ as the structure obtained from I by replacing all atoms pi(A) with ◦(pi(A)) and all atoms qi(A) with •(qi(A)). Define I′′ as the structure that contains the same literals with predicate • as I′ and contains +◦(A) (−◦(A)) whenever it contains +•(A) (−•(A)). Thus the literals with predicate ◦ are chosen in I′′ such that it satisfies SYNC. The following statements are then equivalent: hI, βi |= SM(cnv(F )). hI, βi |= project(CIRC[F [P, Q]; P ; ∅] ∧ (P ↔ Q), Pˆ). hI′, βi |= project(CIRC[F [◦, •]; ◦; ∅] ∧ SYNC, ˆ◦). hI′, βi |= project(CIRC[F ; ◦; ∅] ∧ SYNC, ˆ◦). hI′′, βi |= CIRC[F ; ◦; ∅] ∧ SYNC. hI′′, βi |= circ(F, POS ∪ •ˆ) ∧ SYNC. hI′′, βi |= ans(F ). (vii) (viii) (ix) (x) (xi) (xii) (xiii) 8
We have introduced an operator raise which can be used to define circumscription in a compact way. The definition of that operator – in a semantic framework where structures are represented by sets of literals – is identical to that of literal projection, except that a set inclusion is replaced by a proper set inclusion.
An approach to an intuitive understanding of the raise operator is to consider minimization as passed through from the “object language level” (the extents of predicates is minimized) to the “meta level” of the semantic framework: Raise expresses that model agreement conditions are minimized. Accordingly, the predicate minimization conditions (commonly abbreviated by P ′ < P in definitions of circumscription) have not to be made explicit with the raise operator, but are “built-in”. In addition, the approach to “minimize model agreement conditions” effects that the raise operator straightforwardly covers certain generalizations of circumscription: Raise has – aside of a formula – just a set of literals as argument, such that, depending on the composition of this set, not only parallel circumscription with varied predicates can be expressed, but also predicate maximization conditions. Moreover, also minimization, maximization and agreement conditions can be expressed that apply only to a subset of the instances of a predicate.
The characterization of circumscription in terms of the raise operator is immediately useful to prove properties of circumscription in a streamlined way. The introduced semantic framework with the project and raise operators is a basis for future research, including the further elaboration of common and differing properties of both operators, the exploration of applications that involve combinations of circumscription and projection, and the investigation of possibilities for transferring and interleaving methods for non-monotonic reasoning, such as computation of stable models, with methods for second-order quantifier elimination and the closely related projection computation.