=Paper=
{{Paper
|id=Vol-556/paper-8
|storemode=property
|title=Literal Projection and Circumscription
|pdfUrl=https://ceur-ws.org/Vol-556/paper07.pdf
|volume=Vol-556
|dblpUrl=https://dblp.org/rec/conf/ftp/Wernhard09
}}
==Literal Projection and Circumscription==
https://ceur-ws.org/Vol-556/paper07.pdf
Literal Projection and Circumscription
Christoph Wernhard
Technische Universität Dresden
christoph.wernhard@tu-dresden.de
Abstract. We develop a formal framework intended as a preliminary
step for a single knowledge representation system that provides differ-
ent representation techniques in a unified way. In particular we consider
first-order logic extended by techniques for second-order quantifier elim-
ination 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 circum-
scription 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.
1 Introduction
We develop a formal framework intended as a preliminary step for a single knowl-
edge 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 [5]), including abduction,
modularization of knowledge bases and the processing of circumscription. It
is also closely related to knowledge compilation [13]. Variants of second-order
quantifier elimination also appear under names such as computation of uniform
interpolants, forgetting, and projection. Restricted to propositional formulas it is
called elimination of Boolean quantified variables.
We focus here on a particular generalization of second-order quantifier elim-
ination, the computation of literal projection [10, 11]. Literal projection general-
izes second-order quantification by permitting, so to speak, to quantify upon an
arbitrary set of ground literals, instead of just (all ground literals with) a given
predicate symbol. Literal projection allows, for example, to express predicate
quantification upon a predicate just in positive or negative polarity. Eliminating
such a quantifier from a formula in negation normal form results in a formula
that might still contain the quantified predicate, but only in literals whose po-
larity is complementary to the quantified one. This polarity dependent behavior
of literal projection is essential for the relationship to non-monotonic reasoning
that is investigated in this paper.
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 ex-
pressed as a second-order quantifier elimination task [1]. The formalization of
circumscription investigated here does not just rely on literal projection as a
generalization of second-order quantification, but utilizes the polarity depen-
dent behavior of literal projection to obtain a particular straightforward and
compact characterization. The concrete contributions of this paper are:
– The introduction of an operator raise that is only slightly different from
literal projection and can be used to define a generalization of parallel cir-
cumscription with varied predicates in a straightforward and compact way.
Like literal projection, the raise operator is defined in terms of semantic prop-
erties only, and is thus independent of syntactic properties or constructions.
Some properties of this operator and circumscription, also in interaction with
literal projection, are then shown (Sect. 3–6).
– The characterization of consequences of circumscribed formulas in terms of
literal projection. We make a known result given in [7] more precise and gen-
eralize it from propositional to first-order formulas. In the extended report
version of this paper [12] we provide a thorough proof (Sect. 6).
– A definition of answer sets according to the stable model semantics in terms
of circumscription. Unlike the common definitions of stable models, it does
not recur onto syntactic notions like reduct and fixed-point construction.
It is essentially an adaption of the “circumscription-like” definition recently
proposed in [3, 4]. In contrast to that definition, it does not involve a specially
interpreted rule forming connective (Sect. 7).
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 [12].
61
2 Notation and Preliminaries
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 con-
structed from first-order literals, truth value constants ⊤, ⊥, the unary connec-
tive ¬, 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 [10]
(see also Sect. 4 below). It will be further discussed in this introductory section
(see [10, 11] for more thorough material). The semantics of the raise operator
will be introduced later on in Sect. 3.
Interpretations. We use the notational variant of the framework of Herbrand
interpretations described in [10]: An interpretation I is a pair hI, βi, where I is
a structure, that is, a set of ground literals that contains for all ground atoms A
exactly one of +A or −A, and β is a variable assignment, that is, a mapping of
the set of variables into TERMS.
62
Satisfaction Relation and Semantics of Projection. The satisfaction re-
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 occur-
ring 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 satis-
fies 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.
Table 1. The Satisfaction Relation with the Semantic Definition of Literal Projection
hI, βi |= L iff def Lβ ∈ I
hI, βi |= ⊤
hI, βi 6|= ⊥
hI, βi |= ¬F iff def hI, βi 6|= F
hI, βi |= F1 ∧ F2 iff def hI, βi |= F1 and hI, βi |= F2
hI, βi |= F1 ∨ F2 iff def hI, βi |= F1 or hI, βi |= F2
hI, βi |= ∀x F iff def for all t ∈ TERMS it holds that hI, β xt i |= F
hI, βi |= ∃x F iff def there exists a t ∈ TERMS such that hI, β xt i |= F
hI, βi |= project(F, S) iff def there exists a J such that hJ, βi |= F and J ∩ S ⊆ I
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 in-
terpretation hI, βi is called “structure”, since it can be considered as repre-
sentation 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 , ..., tn i | +p(t1 , ..., tn ) ∈ I}. Moreover, an interpretation hI, βi represents a
conventional second-order interpretation [2] (if predicate variables are considered
as distinguished predicate symbols): The structure in the conventional sense cor-
responds to I, as described above, except that mappings of predicate variables
are omitted. The assignment is β, extended such that all predicate variables p
are mapped to {ht1 , ..., tn i | +p(t1 , ..., tn ) ∈ I}.
63
Some More Notation. The following table specifies symbolic notation for
(i) the complement of a literal, (ii) the set of complement literals of a given set
of literals, (iii) the set complement of a set of ground literals, (iv) the set of all
positive ground literals, (v) the set of all negative ground literals, (vi) the set of
all ground literals whose predicate symbol is from a given set, and (vii, viii) a
structure that is like a given one, except that it assigns given truth values to a
single given ground atom or to all ground atoms in a given set, respectively.
(i) g def
+A g def
= −A; −A = +A. The literal L e is called the complement of L.
(ii) e def e
S = {L | L ∈ S}.
(iii) S def
= ALL − S.
(iv) POS def = {+A | +A ∈ ALL}.
(v) NEG def = {−A | −A ∈ ALL}.
(vi) P̂ is the set of all ground literals whose predicate is P or is in P , resp.,
where P is a predicate symbol, or a tuple or set of predicate symbols.
(vii) I[L] def e ∪ {L}.
= (I − {L})
def f
(viii) I[M ] = (I − M ) ∪ M.
Literal Base and Related Concepts. The literal base L(F ) of a first-order
formula F in negation normal form is the set of all ground instances of lit-
erals in F . The following formal definition generalizes this notion straightfor-
wardly 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(⊤) def
= L(⊥) def= {}; L(¬F ) def ]); L(F ⊗ G) def
= L(F = L(F ) ∪ L(G) if ⊗ is ∧ or
def def
∨; L(⊗xF ) = L(⊗(F, S)) = 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 some-
thing” its essential literal base, made precise in Def. 1 (see [10, 11] for a more
thorough discussion). It can be proven that essential literal base of a formula is
a subset of its literal base. The essential literal base is independent of syntactic
properties: equivalent formulas have the same essential literal base.
Definition 1 (Essential Literal Base). The essential literal base of a for-
mula F, in symbols LE (F ), is defined as LE (F ) def
= {L | L ∈ ALL and there exists
e βi 6|= F }.
an interpretation hI, βi such that hI, βi |= F and hI[L],
Properties of Literal Projection. A summary of properties of literal pro-
jection is displayed in Tab. 2 and 3. Most of them follow straightforwardly from
the semantic definition of project shown in Tab. 1 [11]. The more involved proof
of Tab. 2.xxi (and the related Tab. 3.v) can be found in [10, 11]. The properties
in Tab. 3 strengthen properties in Tab. 2, but apply only to formulas that sat-
isfy a condition related to their essential literal base. These formulas are called
E-formulas and are defined as follows:
Definition 2 (E-Formula). A formula F is called E-formula if and only if
for all interpretations hI, βi and consistent sets of ground literals M such that
hI, βi |= F and M ∩ LE (F ) = ∅ it holds that hI[M f], βi |= F.
64
First-order formulas in negation normal form without existential quantifier –
including propositional formulas and first-order clausal formulas – are E-formu-
las. Being an E-formula is a property that just depends on the semantics of a
formula, that is, an equivalent to an E-formula is also an E-formula. See [10, 11]
for more discussion.1
Table 2. Properties of Literal Projection
(i)
F |= project(F, S)
(ii)
If F1 |= F2 , then project(F1 , S) |= project(F2 , S)
(iii)
If F1 ≡ F2 , then project(F1 , S) ≡ project(F2 , S)
(iv)If S1 ⊇ S2 , then project(F, S1 ) |= project(F, S2 )
(v)project(project(F, S1 ), S2 ) ≡ project(F, S1 ∩ S2 )
(vi)F1 |= project(F2 , S) if and only if project(F1 , S) |= project(F2 , S)
(vii)project(F, ALL) ≡ F
(viii)project(F, L(F )) ≡ F
(ix)project(⊤, S) ≡ ⊤
(x)project(⊥, S) ≡ ⊥
(xi)F is satisfiable if and only if project(F, S) is satisfiable
(xii)LE (project(F, S)) ⊆ S
(xiii)LE (project(F, S)) ⊆ LE (F )
(xiv) If project(F, S) |= F, then LE (F ) ⊆ S
(xv) project(F, S) ≡ project(F, L(F ) ∩ S)
(xvi) F1 |= F2 if and only if project(F1 , L(F2 )) |= F2
(xvii) If no instance of L is in S, then project(L, S) ≡ ⊤
(xviii) If all instances of L are in S, then project(L, S) ≡ L
(xix) project(F1 ∨ F2 , S) ≡ project(F1 , S) ∨ project(F2 , S)
(xx) project(F1 ∧ F2 , S) |= project(F1 , S) ∧ project(F2 , S)
^
(xxi) If L(F1 ) ∩ L(F e
2 ) ⊆ S ∩ S then
project(F1 ∧ F2 , S) ≡ project(F1 , S) ∧ project(F2 , S)
(xxii) project(∃xF, S) ≡ ∃x project(F, S)
(xxiii) project(∀xF, S) |= ∀x project(F, S)
Table 3. Properties of Literal Projection for E-Formulas E
(i) project(E, LE (E)) ≡ E (strengthens Tab. 2.viii)
(ii) LE (E) ⊆ S if and only if project(E, S) ≡ E (strengthens Tab. 2.xiv)
(iii) project(E, S) ≡ project(E, LE (E) ∩ S) (strengthens Tab. 2.xv)
(iv) F |= E if and only if project(F, LE (E)) |= E (strengthens Tab. 2.xvi)
(v) If LE (E1 ) ∩ L^ e
E (E2 ) ⊆ S ∩ S then
project(E1 ∧ E2 , S) ≡ project(E1 , S) ∧ project(E2 , S) (strengthens Tab. 2.xxi)
1
An example that is not an E-formula is the sentence F def = ∀x +r(x, f(x)) ∧
∀x∀y(−r(x, y) ∨ +r(x, f(y))) ∧ ∃x∀y(−r(x, y) ∨ +p(y)). Let the domain be the set
of all terms f n (a) where n ≥ 0. For each member T of the domain it can be verified
that +p(T ) ∈/ LE (F ). On the other hand, an interpretation that contains −p(T ) for
all members T of the domain cannot be a model of F .
65
3 The Raise Operator
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 circum-
scription with varied predicates in a straightforward and compact way.
Definition 3 (Raise).
hI, βi |= raise(F, S) iff def 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 mono-
tonic (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). Proposi-
tion 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 inconsis-
tent. 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 projec-
tion in terms of raise and atom projection [10], a restricted form of projection
where the polarity of the scope members is not taken into account, which can
be expressed as literal projection onto scopes S constrained by S = S. e
Proposition 1 (Properties of Raise).
(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 = S,e 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 ∪ S) e ∨ raise(F, S).
66
4 Definition of Circumscription in Terms of Raise
The following definition specifies a formula circ(F, S) that provides a characteri-
zation of circumscription in terms of raise, as we will first outline informally and
then show more precisely.
Definition 4 (Circumscription).
circ(F, S) def
= F ∧ ¬raise(F, S).
In this notation, the parallel circumscription of predicate constants P in sen-
tence F with varied predicate constants Z [8] is expressed as circ(F, S), where S
is the set of all ground literals L such that either
1. L is positive and its predicate is in P, or
2. The predicate of L is neither in P nor in 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, maximiza-
tion 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 cir-
cumscription by means of second-order quantification [8, 1, 5]. The following
definition specifies a second-order sentence CIRC[F ; P ; Z] that is called paral-
lel circumscription of predicate constants P in F with varied predicate constants
Z in [8] and is straightforwardly equivalent to the sentence called second-order
circumscription of P in F with variable Z in [1, 5]:
Definition 5 (Second-Order Circumscription). Let F be a first-order sen-
tence and let P, P ′ , Z, Z ′ be mutually disjoint tuples of distinct predicate symbols
such that: P = p1 , . . . , pn and P ′ = p′1 , . . . , p′n where n ≥ 0; both Z and Z ′ have
the same length ≥ 0; members of P ′ and P with the same index, as well as
members of Z ′ and Z with the same index, are of the same arity; and P ′ and Z ′
do not contain predicate symbols in F . Let F ′ be the formula that is obtained
from F by replacing each predicate symbol that is in P or Z by the predicate
symbol with the same index in P ′ or Z ′ , respectively. For i ∈ {1, . . . , n} let xi
stand for x1 , . . . , xk , where k is the arity of predicate symbol pi . Let P ′< P stand
for
^ n n
^
∀xi (p′i (xi ) → pi (xi )) ∧ ¬ ∀xi (p′i (xi ) ↔ pi (xi ))).
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:
= F ∧ ¬∃P ′ , Z ′ (F ′ ∧ P ′< P ).
CIRC[F ; P ; Z] def
67
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 pred-
icate symbol occurs in G. Accordingly, CIRC[F ; P ; Z] can be expressed straight-
forwardly in terms of literal projection instead of the second-order quantification:
Definition 6 (Second-Order Circumscription in Terms of Projection).
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:
= F ∧ ¬project(F ′ ∧ P ′< P, P̂ ∪ Q̂).
CIRC-PROJ[F ; P ; Z] def
The Q parameter in Def. 6 is the set of the “fixed” predicates. The set of liter-
als (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 [12] formally relates second-order circum-
scription expressed by projection (Def. 6) with circumscription defined in terms
of of the raise operator (Def. 4).
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 Well-Foundedness
As discussed in [8], circumscription can in general only be applied usefully to a
sentence F if all models of F extend some model of F that is minimal with respect
to the circumscribed predicates. The concept of well-foundedness [8] makes this
property precise. We show that it can be expressed in a compact way in terms of
projection. This characterization facilitates to prove properties of circumscrip-
tion that have well-foundedness as a precondition, as for example Prop. 3 and
Theorem 2 below.
68
Definition 7 (Well-Founded Formula). F is called well-founded with respect
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, corre-
sponding to variants of circumscription as indicated in Sect. 4. We now explicate
how this definition renders the definition of well-foundedness in [8], which is de-
fined for the special case of circumscription of a single predicate p with varied
predicates Z. That definition is as as follows (adapted to our notation): Let F
be a first-order sentence, p be predicate symbol and Z be a tuple of predicate
symbols. The sentence F is called well-founded with respect to (p; Z) if for every
model I of F there exists a model J of CIRC[F ; p; Z] such that I and J differ only
in how they interpret p and Z and the extent of p in J is a (not necessarily strict)
subset of its extent in I. We can convert this definition straightforwardly into our
semantic framework: Let Q be the set of predicate symbols in F that are different
from p and not in Z. The sentence F is then well-founded with respect to (p; Z)
if for all interpretations hI, βi such that hI, βi |= F there exists an interpreta-
tion hJ, βi such that (1.) hJ, βi |= CIRC-PROJ[F ; p; Z], (2.) J ∩ p̂ ∩ POS ⊆ ∩I,
and (3.) J ∩ Q̂ = I ∩ Q̂. The project operator allows to express this converted
definition compactly: Let S be the literal scope ((p̂ ∩ POS) ∪ Q̂). By Theorem 1,
CIRC-PROJ[F ; p; Z] is equivalent to circ(F, S). Furthermore, given that I and J
ê
are structures and Q̂ = Q, the conjunction of items (2.) and (3.) above is equiv-
alent to J ∩ S ⊆ I. By the definition of project (Tab. 1), the statement that
there exists an interpretation hJ, βi satisfying items (1.)–(3.) can be expressed
as hI, βi |= project(circ(F, S), S).
6 Interplay of Projection and Circumscription
The following proposition shows properties of projection nested within circum-
scription. It is independent of the well-founded property.
Proposition 2 (Circumscribing Projections).
(i) circ(F, S) |= circ(project(F, S), S).
e S).
(ii) circ(project(F, S), S) |= circ(project(F, S ∪ 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 equiva-
lence 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).
69
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.
Proposition 3 (Projecting Circumscriptions). If F is well-founded with
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 lit-
eral 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 posi-
tive 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 comput-
ing 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 rep-
resentation of such a formula F ′ [13].
Literal forgetting is a variant of literal projection that can be defined as
forget(F, S) def
= project(F, S) and is investigated for propositional logic in [7]. It
is shown there that circumscription, or more precisely the formulas that are
entailed by circumscriptions, can be characterized in terms of literal forgetting.
Two such characterizations are given as Proposition 22 in [7], where the simpler
one applies if the literal base of the entailed formula is restricted in a certain
way.
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 [7] in the following four respects: (1.) We use weaker re-
quirements on the entailed formulas by referring to the essential literal base
instead of the (syntactic) literal base. The respective requirements on the syn-
tactic literal base follow, since it is a subset of the essential literal base (see
Sect. 2). (2.) We provide a thorough proof in [12]. The proof given in [7] just
shows the characterizations as straightforward consequence of [9, Theorems 2.5
and 2.6], for which in turn no proof is given, neither in [9], nor in [6] which
is referenced by [9]. (3.) We generalize the characterizations to first-order logic.
(4.) We add a third basic variant (Theorem 2.i) for consequents that are stronger
restricted than in Theorem 2.ii.
This basic variant is actually a straightforward generalization of Proposi-
tion 12 in [8], which is introduced as capturing the intuition that, under the
assumption of well-foundedness, a circumscription provides no new information
about the fixed predicates, and only “negative” additional information about
the circumscribed predicates.
70
Theorem 2 (Consequences of Circumscription). If F is well-founded with
respect to S, then
circ(F, S) |= G
is equivalent to (at least) one of the following statements, depending on LE (G):
(i) F |= G, if LE (G) ⊆ S;
(ii) F |= project(F ∧ G, S), e
if LE (G) ⊆ (S ∪ S);
(iii) F |= project(F ∧ ¬project(F ∧ ¬G, S), S).
7 Answer Sets with Stable Model Semantics
In [3, 4] a characterization of stable models in terms of a formula translation
that is similar to the second-order circumscription has been presented. Roughly,
it differs from circumscription in that only certain occurrences of predicates
are circumscribed, which are identified by their position with respect to a non-
classical rule forming operator. We develop a variant of this characterization of
stable models that is in terms of circumscription. It involves no non-classical
operators. Instead, to indicate occurrences be circumscribed, it puts atoms into
term position, wrapped by one of two special predicates.
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 con-
ventional 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. W
m
Wn(ii) For a rule clause of the form specified in (8.i), the rule
Wo clause ( Wi=1 −◦Ai ∨
p
i=1 +•B i ) is called its negated body, and the rule clause ( i=1 +◦C i ∨ i=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 vari-
ables. The implicit quantifier prefixes of clauses are not written in this definition.
71
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.
Definition 9 (Answer Set). For all logic programs F :
ans(F ) def
= circ(F, POS ∪ ˆ•) ∧ SYNC.
In the definition of ans(F ), the scope of the circumscription, (POS ∪ ˆ•), is equal
◦ ∩ POS) ∪ ˆ
to ((ˆ •) 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 [3, 4], and justify in this way that ans(F )
indeed characterizes stable models. More detailed proofs and relationships to
reduct based characterizations of answer sets can be found in [12]. We limit
our considerations to logic programs according to Def. 8.iii, which are clausal
sentences (the characterization in [3, 4] applies also to nonclausal sentences).
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 non-
classical operators used by [3, 4] (see [12] for an explicit such conversion). Let
SM(cnv(F )) be the second-order sentence that characterizes the stable models
of cnv(F ) according to [3, 4]. The following equivalence can be verified, where
P ′< P has the same meaning as in Def. 5:
SM(cnv(F )) ≡ F [P, P ] ∧ ¬∃P ′ (F [P ′ , P ] ∧ P ′< P ). (ii)
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 Vnand add the requirement that
P and Q are equivalent: Let (P ↔ Q) stand for 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) (iii)
≡ F [P, Q] ∧ ¬∃P ′ (F [P ′ , Q] ∧ P ′< P ) ∧ (P ↔ Q) (iv)
≡ CIRC[F [P, Q]; P ; ∅] ∧ (P ↔ Q). (v)
72
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 )). (vii)
hI, βi |= project(CIRC[F [P, Q]; P ; ∅] ∧ (P ↔ Q), P̂ ). (viii)
hI ′ , βi |= project(CIRC[F [◦, •]; ◦; ∅] ∧ SYNC, ◦ˆ). (ix)
hI ′ , βi |= project(CIRC[F ; ◦; ∅] ∧ SYNC, ◦ˆ). (x)
hI ′′ , βi |= CIRC[F ; ◦; ∅] ∧ SYNC. (xi)
hI ′′ , βi |= circ(F, POS ∪ ˆ•) ∧ SYNC. (xii)
hI ′′ , βi |= ans(F ). (xiii)
8 Conclusion
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 pred-
icate 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 ar-
gument, such that, depending on the composition of this set, not only parallel
circumscription with varied predicates can be expressed, but also predicate maxi-
mization conditions. Moreover, also minimization, maximization and agreement
conditions can be expressed that apply only to a subset of the instances of a
predicate.
73
The characterization of circumscription in terms of the raise operator is im-
mediately 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 dif-
fering properties of both operators, the exploration of applications that involve
combinations of circumscription and projection, and the investigation of possi-
bilities 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.
References
1. P. Doherty, W. Lukaszewicz, and A. Szalas. Computing circumscription revisited:
A reduction algorithm. J. Autom. Reason., 18(3):297–338, 1997.
2. H.-D. Ebbinghaus, J. Flum, and W. Thomas. Einführung in die mathematische
Logik. Spektrum Akademischer Verlag, Heidelberg, 4th edition, 1996.
3. P. Ferraris, J. Lee, and V. Lifschitz. A new perspective on stable models. In
IJCAI-07, pages 372–379, 2007.
4. P. Ferraris, J. Lee, and V. Lifschitz. Stable models and circumscription. 2009.
To appear; Draft retrieved on May 17th 2009 from https://www.cs.utexas.edu/
users/otto/papers/smcirc.pdf.
5. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second-Order Quantifier Elimination:
Foundations, Computational Aspects and Applications. CollegePublications, 2008.
6. M. Gelfond, H. Przymusinska, and T. Przymusinski. The extended closed world
assumption and its relationship to parallel circumscription. In ACM SIGACT-
SIGMOD Symposium on Principles of Database Systems, pages 133–139, 1986.
7. J. Lang, P. Liberatore, and P. Marquis. Propositional independence – formula-
variable independence and forgetting. JAIR, 18:391–443, 2003.
8. V. Lifschitz. Circumscription. In Handbook of Logic in AI and Logic Programming,
volume 3, pages 298–352. Oxford University Press, 1994.
9. T. Przymusinski. An algorithm to compute circumscription. Artificial Intelligence,
83:59–73, 1989.
10. C. Wernhard. Literal projection for first-order logic. In JELIA 08, pages 389–402,
2008.
11. C. Wernhard. Automated Deduction for Projection Elimination. Number 324 in
Dissertationen zur Künstlichen Intelligenz (DISKI). AKA/IOS Press, 2009.
12. C. Wernhard. Literal projection and circumscription – extended version.
Technical report, Technische Universität Dresden, 2009. Available from
http://cs.christophwernhard.com/papers/projection-circumscription.pdf.
13. C. Wernhard. Tableaux for projection computation and knowledge compilation.
In TABLEAUX 2009, pages 325–340, 2009.
74