Founded Semantics and Constraint Semantics of Logic Rules∗

arXiv:1606.06269v3 [cs.LO] 15 Apr 2017

Yanhong A. Liu
Scott D. Stoller
Computer Science Department, Stony Brook University
{liu,stoller}@cs.stonybrook.edu
Abstract
This paper describes a simple new semantics for logic rules, founded semantics, and its
straightforward extension to another simple new semantics, constraint semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates
and rules to be specified explicitly. They are completely declarative and easy to understand and
relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time
in the size of the ground program.

Keywords: Datalog, non-stratified negation, existential and universal quantifications, constraints,
well-founded semantics, stable model semantics, Fitting (Kripke-Kleene) semantics, supported model
semantics

1

Introduction

Logic rules and inference are fundamental in computer science, especially for solving complex modeling, reasoning, and analysis problems in critical areas such as program verification, security, and
decision support.
The semantics of logic rules and their efficient computations have been a subject of significant
study, especially for complex rules that involve recursive definitions and unrestricted negation and
quantifications. Many different semantics and computation methods have been proposed. Even
the two dominant semantics for logic programs, well-founded semantics (WFS) [VRS91, VG93] and
stable model semantics (SMS) [GL88], are still difficult to understand intuitively, even for extremely
simple rules; they also make implicit assumptions and, in some cases, do not capture common sense,
especially ignorance.
This paper describes a simple new semantics for logic rules, founded semantics, that extends
straightforwardly to another simple new semantics, constraint semantics.
• The new semantics support unrestricted negation (both stratified and non-stratified), as well
as unrestricted combinations of existential and universal quantifications.
• They allow each predicate to be specified explicitly as certain (each assertion of the predicate
has one of two values: true, false) or uncertain (has one of three values: true, false, undefined),
and as complete (all rules defining the predicate are given) or not.
• Completion rules are added for predicates that are complete, as explicit rules for inferring the
negation of those predicates using the negation of the hypotheses of the given rules.
∗

This work was supported in part by NSF under grants CCF-1414078, CNS-1421893, IIS-1447549, CCF-1248184,
CCF-0964196, and CCF-0613913; and ONR under grants N000141512208 and N000140910651.

1

• Founded semantics infers all true and false values that are founded, i.e., rooted in the given
true or false values and exactly following the rules, and it completes certain predicates with
false values and completes uncertain predicates with undefined values.
• Constraint semantics extends founded semantics by allowing undefined values to take all combinations of true and false values that satisfy the constraints imposed by the rules.
Founded semantics and constraint semantics unify the core of previous semantics and have three
main advantages:
1. They are expressive and intuitive, by allowing assumptions about predicates and rules to be
specified explicitly, by including the choice of uncertain predicates to support common-sense
reasoning with ignorance, and by adding explicit completion rules to define the negation of
predicates.
2. They are completely declarative and easy to understand. Founded semantics takes the given
rules and completion rules as recursive definitions of the predicates and their negation, and
is simply the least fixed point of the recursive functions. Constraint semantics takes the
given rules and completion rules as constraints, and is simply the set of all solutions that are
consistent with founded semantics.
3. They relate cleanly to prior semantics, including WFS and SMS, as well as Fitting semantics
(also called Kripke-Kleene semantics) [Fit85], supported models [ABW88], stratified semantics [ABW88, VG89], and first-order logic, by explicitly specifying corresponding assumptions
about the predicates and rules.
Additionally, founded semantics can be computed in linear time in the size of the ground program,
as opposed to quadratic time for WFS.
Finally, founded semantics and constraint semantics can be extended to allow uncertain, complete predicates to be specified as closed—making an assertion of the predicate false if inferring it
to be true (respectively false) using the given rules and facts requires assuming itself to be true
(respectively false)—and thus match WFS and SMS, respectively.

2

Motivation for founded semantics and constraint semantics

Founded semantics and constraint semantics are designed to be intuitive and expressive. For rules
with no negation or with restricted negation, which have universally accepted semantics, the new
semantics are consistent with the accepted semantics. For rules with unrestricted negation, which
so far lack a universally accepted semantics, the new semantics unify the core of prior semantics
with two basic principles:
1. Assumptions about certain and uncertain predicates, with true (T ) and false (F ) values,
or possibly undefined (U ) values, and about whether the rules defining each predicate are
complete must be made explicit.
2. Any easy-to-understand semantics must be consistent with one where everything inferred that
has a unique T or F value is rooted in the given T or F values and following the rules.
This section gives informal explanations.
Rules with no negation. Consider a set of rules with no negation in the hypotheses, e.g., a
rule can be “ q(x) if p(x)” but not “ q(x) if not p(x)” for predicates p and q and variable x. The
meaning of the rules, given a set of facts, e.g., a fact p(a) for constant a, is the set of all facts that
2

are given or can be inferred by applying the rules to the facts, e.g., {p(a),q(a)} using the example
rule and fact given. In particular,
1. Everything is either T or F , i.e., T as given or inferred facts, or F as otherwise. So one can
just explicitly express what are T , and the rest are F .
2. Everything inferred must be founded, i.e., rooted in the given facts and following the rules.
So anything that always depends on itself, e.g., p(a), given only the rule “ p(x) if p(x)”, is
not T .
In technical terms, the semantics is 2-valued, and the set of all facts, i.e., true assertions, is the
minimum model, equal to the least fixed point of applying the rules starting from the given facts.
Rules with restricted negation. Consider rules with negation in the hypotheses, but with each
negation only on a predicate all of whose facts can be inferred without using the rule containing
that negation, e.g., one can have “ q(x) if not p(x)” but not “ p(x) if not p(x)”. The meaning of
the rules is as for rules with no negation except that a rule with negation is applied only after all
facts of the negated predicates have been inferred. In other words,
The true assertions of any predicate do not depend on the negation of that predicate. So a
negation could be just a test after all facts of the negated predicate are inferred. The rest
remains the same as for rules with no negation.
In technical terms, this is stratified negation; the semantics is still 2-valued, the minimum model,
and the set of all true assertions is the least fixed point of applying the rules in order of the strata.
Rules with unrestricted negation. Consider rules with unrestricted negation in the hypotheses,
where a predicate may cyclically depend on its own negation, e.g., “ p(x) if not p(x)”. Now the
value of a negated assertion needs to be established before all facts of the negated predicate have
been inferred. In particular,
There may not be a unique T or F value for each assertion. For example, given only rule
“ p(x) if not p(x)”, p(a) cannot be T because inferring it following the rule would require
itself be F , and it cannot be F because it would lead to itself being T following the rule. That
is, there may not be a unique 2-valued model.
In technical terms, the negation may be non-stratified. There are two best solutions to this that
generalize a unique 2-valued model: a unique 3-valued model and a set of 2-valued models, as in
the dominant well-founded semantics (WFS) and stable model semantics (SMS), respectively.
In a unique 3-valued model, when a unique T or F value cannot be established for an assertion,
a third value, undefined (U ), is used. For example, given only rule “ p(x) if not p(x)”, p(a) is U ,
in both WFS and founded semantics.
• With the semantics being 3-valued, when one cannot infer that an assertion is T , one should
be able to express whether it is F or U when there is a choice. For example, given only rule
“ p(x) if p(x)”, p(a) is not T , so p(a) may in general be F or U .
• WFS requires that such an assertion be F , even though common sense generally says that it
is U . WFS attempts to be the same as in the case of 2-valued semantics, even though one is
now in a 3-valued situation.
• Founded semantics supports both, allowing one to choose explicitly when there is a choice.
Founded semantics is more expressive by supporting the choice. It is also more intuitive by
supporting the common-sense choice for expressing ignorance.
3

For a set of 2-valued models, similar considerations motivate our constraint semantics. In particular, given only rule “ p(x) if not p(x)”, the semantics is the empty set, in both SMS and constraint
semantics, because no model can contain p(a) or not p(a), for any a, because p(a) cannot be T or
F as discussed above. However, given only rule “ p(x) if p(x)”, SMS requires that p(a) be F in all
models, while constraint semantics allows the choice of p(a) being F in all models or being T in
some models.
Certain or uncertain. Founded semantics and constraint semantics first allow a predicate to
be declared certain (i.e., each assertion of the predicate has one of two values: T , F ) or uncertain
(i.e., each assertion of the predicate has one of three values: T , F , U ) when there is a choice. If
a predicate is defined (as conclusions of rules) with use of non-stratified negation, then it must
be declared uncertain, because it might not have a unique 2-valued model. Otherwise, it may be
declared certain or uncertain.
• For a certain predicate, everything T must be given or inferred by following the rules, and the
rest are F , in both founded semantics and constraint semantics.
• For an uncertain predicate, everything T or F must be given or inferred, and the rest are U
in founded semantics. Constraints semantics then extends everything U to be combinations
of T and F that satisfy all the rules and facts as constraints.
Complete or not. Founded semantics and constraint semantics then allow an uncertain predicate
that is in the conclusion of a rule to be declared complete, i.e., all rules with that predicate in the
conclusion are given.
• If a predicate is complete, then completion rules are added to define the negation of the
predicate explicitly using the negation of the hypotheses of all given rules and facts of that
predicates.
• Completion rules, if any, and given rules are used together to infer everything T and F . The
rest are U in founded semantics, or are combinations of T and F in constraint semantics as
described above.
Closed or not. Finally, founded semantics and constraint semantics can be extended to allow
an uncertain, complete predicate to be declared closed, i.e., an assertion of the predicate is made
F , called self-false, if inferring it to be T (respectively F ) using the given rules and facts requires
assuming itself to be T (respectively F ).
• Determining self-false assertions is similar to determining unfounded sets in WFS. Repeatedly
computing founded semantics and self-false assertions until a least fixed point is reached yields
WFS.
• Among combinations of T and F values for assertions with U values in WFS, removing each
combination that has self-false assertions that are not already F in that combination yields
SMS.
Correspondence to prior semantics, more on motivation. Table 1 summarizes corresponding declarations for different assumptions under prior semantics; formal definitions and proofs for
these and for additional relationships appear in the following sections. Founded semantics and
constraint semantics allow additional combinations of declarations than those in the table.

4

Prior Semantics
Stratified
First-Order Logic
Fitting (Kripke-Kleene)
Supported
WFS
SMS

Kinds of Rules

New
no non-stratified Founded
negation
Constraint
any
any
any

Constraint

Certain?

Complete?

Closed?

Theorem

yes

(implied
yes)

(implied
yes)

5

no

no

(implied
no)

6

yes

no

yes

yes

Founded
no except for
Constraint extensional pred’s
Founded
any allowed
Constraint

7
11
17
18

Table 1: Declarations, for all predicates, for different assumptions under prior semantics.
Some observations from the table may help one better understand founded semantics and constraint semantics.
• The top 4 wide rows cover all combinations of allowed declarations (for all predicates).
• Wide row 1 is a special case of wide row 4, because being certain implies being complete
and closed. So one could prefer to use only the latter two choices and omit the first choice.
However, being certain is uniquely important, both for conceptual simplicity and practical
efficiency:
(1) It covers the vast class of database applications that do not use non-stratified negation,
for which stratified semantics is universally accepted. It does not need to be understood by
explicitly combining the latter two more sophisticated notions.
(2) It allows founded semantics to match WFS for all example programs we found in the
literature, with predicates being certain when possible and complete otherwise, but without
the last, most sophisticated notion of being closed; and the semantics can be computed in
linear time.
• Wide rows 2 and 3 allow the assumption about predicates that are uncertain, not complete,
or not closed to be made explicitly.
In a sense, WFS uses F for both false and some kinds of ignorance (no knowledge of something
must mean it is F ), uses T for both true and some kinds of ignorance inferred through negation
of F , and uses U for conflict, remaining kinds of ignorance from T and F , and imprecision; SMS
resolves the ignorance in U , but not the ignorance in F and T . In contrast,
• founded semantics uses T only for true, F only for false, and U for conflict, ignorance, and
imprecision;
• constraint semantics further differentiates among conflict, ignorance, and imprecision—
corresponding to there being no model, multiple models, and a unique model, respectively,
consistent with founded semantics.
After all, any easy-to-understand semantics must be consistent with the T and F values that
can be inferred by exactly following the rules and completion rules starting from the given facts.
• Founded semantics is the maximum set of such T and F assertions, as a least fixed point of
the given rules and completion rules if any, plus U values for the remaining assertions.
• Constraint semantics is the set of combinations of all T and F assertions that are consistent
with founded semantics and satisfy the rules as constraints.
Founded semantics without closed predicates can be computed easily and efficiently, as a least fixed
point, instead of an alternating fixed point or iterated fixed point for computing WFS.
5

3

Language

We first consider Datalog with unrestricted negation in hypotheses. We extend it in Section 7 to
allow unrestricted combinations of existential and universal quantifications and other features.
Datalog with unrestricted negation. A program in the core language is a finite set of rules of
the following form, where any Pi may be preceded with ¬, and any Pi and Q over all rules may be
declared certain or uncertain, and declared complete or not:
Q(X1 , ..., Xa ) ← P1 (X11 , ..., X1a1 ) ∧ ... ∧ Ph (Xh1 , ..., Xhah )

(1)

Symbols ←, ∧, and ¬ indicate backward implication, conjunction, and negation, respectively; h is
a natural number, each Pi (respectively Q) is a predicate of finite number ai (respectively a) of
arguments, each Xij and Xk is either a constant or a variable, and each variable in the arguments
of Q must also be in the arguments of some Pi .
If h = 0, there is no Pi or Xij , and each Xk must be a constant, in which case Q(X1 , ..., Xa ) is
called a fact. For the rest of the paper, “rule” refers only to the case where h ≥ 1, in which case each
Pi (Xi1 , ..., Xiai ) or ¬Pi (Xi1 , ..., Xiai ) is called a hypothesis of the rule, and Q(X1 , ..., Xa ) is called
the conclusion of the rule. The set of hypotheses of the rule is called the body of the rule.
A predicate declared certain means that each assertion of the predicate has a unique true (T )
or false (F ) value. A predicate declared uncertain means that each assertion of the predicate has a
unique true, false, or undefined (U ) value. A predicate declared complete means that all rules with
that predicate in the conclusion are given in the program.
A predicate in the conclusion of a rule is said to be defined using the predicates or their negation
in the hypotheses of the rule, and this defined-ness relation is transitive.
• A predicate must be declared uncertain if it is defined transitively using its own negation, or
is defined using an uncertain predicate; otherwise, it may be declared certain or uncertain and
is by default certain.
• A predicate may be declared complete or not only if it is uncertain and is in the conclusion
of a rule, and it is by default complete.
In examples with no explicit specification of declarations, default declarations are used.
Rules of form (1) without negation are captured exactly by Datalog [CGT90, AHV95], a database
query language based on the logic programming paradigm. Recursion in Datalog allows queries not
expressible in relational algebra or relational calculus. Negation allows more sophisticated logic
to be expressed directly. However, unrestricted negation in recursion has been the main challenge
in defining the semantics of such a language, e.g., [AB94, Fit02, Tru17], including whether the
semantics should be 2-valued or 3-valued, and whether the rules are considered complete or not.
Example. We use win, the win-not-win game, as a running example, with default declarations:
move is certain, and win is uncertain and complete. A move from position x to position y is represented by a fact move(x,y). The following rule captures the win-not-win game: a position x is
winning if there is a move from x to some position y and y is not winning. Arguments x and y are
variables.
win(x) ← move(x,y) ∧ ¬ win(y)



6

Notations. In arguments of predicates, we use letter sequences for variables, and use numbers
and quoted strings for constants. In presenting the semantics, in particular the completion rules,
we use equality and the notations below for existential and universal quantifications, respectively,
in the hypotheses of rules, and use negation in the conclusions.
∃ X1 , ..., Xn | Y
∀ X1 , ..., Xn | Y

existential quantification
universal quantification

(2)

The quantifications return T iff for some or all, respectively, combinations of values of X1 , ..., Xn ,
the value of Boolean expression Y is T . The domain of each quantified variable is the set of all
constants in the program.

4

Formal definition of founded semantics and constraint semantics

Atoms, literals, and projection. Let π be a program. A predicate is intensional in π if it
appears in the conclusion of at least one rule; otherwise, it is extensional. An atom of π is a formula
formed by applying a predicate symbol in π to constants in π. A literal of π is an atom of π or the
negation of an atom of π. These are called positive literals and negative literals, respectively. The
literals p and ¬p are complements of each other. A set of literals is consistent if it does not contain
a literal and its complement. The projection of a program π onto a set S of predicates, denoted
Proj (π, S), contains all facts of π for predicates in S and all rules of π whose conclusions contain
predicates in S.
Interpretations, ground instances, models, and derivability. An interpretation of π is a
consistent set of literals of π. Interpretations are generally 3-valued: a literal p is true (T ) in
interpretation I if it is in I, is false (F ) in I if its complement is in I, and is undefined (U ) in I if
neither it nor its complement is in I. An interpretation of π is 2-valued if it contains, for each atom
A of π, either A or its complement. An interpretation I is 2-valued for predicate P if, for each atom
A for P , I contains A or its complement. Interpretations are ordered by set inclusion ⊆.
A ground instance of a rule R is any rule that can be obtained from R by expanding universal
quantifications into conjunctions over all constants in the domain, instantiating existential quantifications with constants, and instantiating the remaining variables with constants. For example,
q(a) ← p(a) ∧ r(b) is a ground instance of q(x) ← p(x) ∧ ∃ y | r(y). An interpretation is a model
of a program if it contains all facts in the program and satisfies all rules of the program, interpreted
as formulas in 3-valued logic [Fit85], i.e., for each ground instance of each rule, if the body is true,
then so is the conclusion. The one-step derivability operator Tπ for program π performs one step of
inference using rules of π, starting from a given interpretation. Formally, C ∈ Tπ (I) iff C is a fact
of π or there is a ground instance R of a rule of π with conclusion C such that each hypothesis of
R is true in interpretation I.
Dependency graph. The dependency graph DG(π) of program π is a directed graph with a
node for each predicate of π, and an edge from Q to P labeled + (respectively, −) if a rule whose
conclusion contains Q has a positive (respectively, negative) hypothesis that contains P . If the node
for predicate P is in a cycle containing only positive edges, then P has circular positive dependency
in π; if it is in a cycle containing a negative edge, then P has circular negative dependency in π.

7

Founded semantics. Intuitively, the founded model of a program π, denoted Founded (π), is the
least set of literals that are given as facts or can be inferred by repeated use of the rules. We define
Founded (π) = UnNameNeg(LFPbySCC (NameNeg(Cmpl (π)))), where functions Cmpl , NameNeg,
LFPbySCC , and UnNameNeg are defined as follows.
Completion. The completion function, Cmpl (π), returns the completed program of π. Formally,
Cmpl (π) = AddInv (Combine(π)), where Combine and AddInv are defined as follows.
The function Combine(π) returns the program obtained from π by replacing the facts and rules
defining each uncertain complete predicate Q with a single combined rule for Q, defined as follows.
Transform the facts and rules defining Q so they all have the same conclusion Q(V1 , . . . , Va ), by
replacing each fact or rule Q(X1 , . . . , Xa ) ← H1 ∧ · · · ∧ Hh with Q(V1 , ..., Va ) ← (∃ Y1 , ..., Yk | V1 =
X1 ∧ · · · ∧ Va = Xa ∧ H1 ∧ · · · ∧ Hh ), where V1 , ..., Va are fresh variables (i.e., not occurring in the
given rules defining Q), and Y1 , ..., Yk are all variables occurring in X1 , ..., Xa , H1 , ..., Hh . Combine
the resulting rules for Q into a single rule defining Q whose body is the disjunction of the bodies
of those rules. This combined rule for Q is logically equivalent to the original facts and rules for Q.
Similar completion rules are used in Clark completion [Cla87] and Fitting semantics [Fit85].
Example. For the win example, the rule for win becomes the following. For readability, we
renamed variables to transform the equality conjuncts into identities and then eliminated them.
win(x) ← ∃ y | (move(x,y) ∧ ¬ win(y))


The function AddInv (π) returns the program obtained from π by adding, for each uncertain
complete predicate Q, a completion rule that derives negative literals for Q. The completion rule
for Q is obtained from the inverse of the combined rule defining Q (recall that the inverse of C ← B
is ¬C ← ¬B), by putting the body of the rule in negation normal form, i.e., using identities
of predicate logic to move negation inwards and eliminate double negations, so that negation is
applied only to atoms.
Example. For the win example, the added rule is
¬ win(x) ← ∀ y | (¬ move(x,y) ∨ win(y))



Least fixed point. The least fixed point is preceded and followed by functions that introduce
and remove, respectively, new predicates representing the negations of the original predicates.
The function NameNeg(π) returns the program obtained from π by replacing each negative
literal ¬P (X1 , . . . , Xa ) with n.P (X1 , . . . , Xa ), where the new predicate n.P represents the negation
of predicate P .
Example. For the win example, this yields:
win(x) ← ∃ y | (move(x,y) ∧ n.win(y))
n.win(x) ← ∀ y | (n.move(x,y) ∨ win(y))


The function LFPbySCC (π) uses a least fixed point to infer facts for each strongly connected
component (SCC) in the dependency graph of π, as follows. Let S1 , . . . , Sn be a list of the SCCs
in dependency order, so earlier SCCs do not depend on later ones; it is easy to show that any
linearization of the dependency order leads to the same result for LFPbySCC . For convenience, we
overload S to also denote the set of predicates in the SCC.
Define LFPbySCC (π) = In , where I0 is the empty set and Ii = AddNeg (LFP (TIi−1 ∪Proj (π,Si ) ), Si )
for i ∈ [1..n]. LFP is the least fixed point operator. The least fixed point is well-defined, because the
one-step derivability function TIi−1 ∪Proj (π,Si ) is monotonic, because the program π does not contain
8

negation. The function AddNeg(I, S) returns the interpretation obtained from interpretation I by
adding completion facts for certain predicates in S to I; specifically, for each such predicate P , for
each combination of values v1 , . . . , va of arguments of P , if I does not contain P (v1 , . . . , va ), then
add n.P (v1 , . . . , va ).
Example. For the win example, the least fixed point calculation
1.
2.
3.
4.

infers n.win(x) for any x that does not have move(x,y) for any y, i.e., has no move to anywhere;
infers win(x) for any x that has move(x,y) for some y and n.win(y) has been inferred;
infers more n.win(x) for any x such that any y having move(x,y) has win(y);
repeatedly does 2 and 3 above until a fixed point is reached.


The function UnNameNeg(I) returns the interpretation obtained from interpretation I by replacing each atom n.P (X1 , . . . , Xa ) with ¬P (X1 , . . . , Xa ).
Example. For the win example, positions x for which win(x) is T , F , and U , respectively, in
the founded model correspond exactly to the well-known win, lose, and draw positions, respectively.
In particular,
1. a losing position is one that either does not have a move to anywhere or has moves only to
winning positions;
2. a winning position is one that has a move to a losing position; and
3. a draw position is one not satisfying either case above, i.e., it is in a cycle of moves that do not
have a move to a losing position, called a draw cycle, or is a position that has only sequences
of moves to positions in draw cycles.

Example. If the running example uses the declaration that move is uncertain instead of the
default of being certain, then the founded semantics infers that win is U for all positions.

Constraint semantics. Constraint semantics is a set of 2-valued models based on founded semantics. A constraint model of π is a consistent 2-valued interpretation M such that M is a model
of Cmpl (π) and Founded (π) ⊆ M . Let Constraint (π) denote the set of constraint models of π.
Constraint models can be computed from Founded (π) by iterating over all assignments of true and
false to atoms that are undefined in Founded (π), and checking which of the resulting interpretations
satisfy all rules in Cmpl (π).
Example. For win, draw positions (i.e., positions for which win is undefined) are in draw cycles,
i.e., cycles that do not have a move to a n.win position, or are positions that have only a sequence
of moves to positions in draw cycles.
1. If some SCC has draw cycles of only odd lengths, then there is no satisfying assignment of T
and F to win for positions in the SCC, so there are no constraint models of the program.
2. If some SCC has draw cycles of only even lengths, then there are two satisfying assignments of
T and F to win for positions in the SCC, with the truth values alternating between T and F
around each cycle, and with the second truth assignment obtained from the first by swapping
T and F . The total number of constraint models of the program is exponential in the number
of such SCCs.


5

Properties of founded semantics and constraint semantics

Proofs of theorems appear in Appendix C.
9

Consistency and correctness. The most important properties are consistency and correctness.
Theorem 1 . The founded model and constraint models of a program π are consistent.
Theorem 2 . The founded model of a program π is a model of π and Cmpl (π). The constraint
models of π are 2-valued models of π and Cmpl (π).
Same SCC, same certainty. All predicates in an SCC have the same certainty.
Theorem 3 . For every program, for every SCC S in its dependence graph, all predicates in S are
certain, or all of them are uncertain.
Higher-order programming. Higher-order logic programs, in languages such as HiLog, can be
encoded as first-order logic programs by a semantics-preserving transformation that replaces uses
of the original predicates with uses of a single predicate holds whose first argument is the name
of an original predicate [CKW93]. For example, win(x) is replaced with holds(win,x). This transformation merges a set of predicates into a single predicate, facilitating higher-order programming.
We show that founded semantics and constraint semantics are preserved by merging of compatible
predicates, defined below, if a simple type system is used to distinguish the constants in the original
program from the new constants representing the original predicates.
We extend the language with a simple type system. A type denotes a set of constants. Each
predicate has a type signature that specifies the type of each argument. A program is well-typed
if, in each rule or fact, (1) each constant belongs to the type of the argument where the constant
occurs, and (2) for each variable, all its occurrences are as arguments with the same type. In the
semantics, the values of predicate arguments are restricted to the appropriate type.
Predicates of program π are compatible if they are in the same SCC in DG(π) and have the
same arity, same type signature, and (if uncertain) same completeness declaration. For a set S
of compatible predicates of program π with arity a and type signature T1 , . . . , Ta , the predicatemerge transformation Merge S transforms π into a program Merge S (π) in which predicates in S
are replaced with a single fresh predicate holds whose first parameter ranges over S, and which
has the same completeness declaration as the predicates in S. Each atom A in a rule or fact
of π is replaced with MergeAtom S (A), where the function MergeAtom S on atoms is defined by:
MergeAtom S (P (X1 , . . . , Xa )) equals holds("P ", X1 , . . . , Xa ) if P ∈ S and equals P (X1 , . . . , Xa )
otherwise. We extend MergeAtom S pointwise to a function on sets of atoms and a function on
sets of sets of atoms. The predicate-merge transformation introduces S as a new type. The type
signature of holds is S, T1 , . . . , Ta .
Theorem 4 . Let S be a set of compatible predicates of program π. Then Merge S (π) and π have
the same founded semantics, in the sense that Founded (Merge S (π)) = MergeAtom S (Founded (π)).
Merge S (π) and π also have the same constraint semantics, in the sense that Constraint (Merge S (π))
= MergeAtom S (Constraint (π)).

6

Comparison with other semantics

Stratified semantics. A program π has stratified negation if it does not contain predicates with
circular negative dependencies. Such a program has a well-known and widely accepted semantics
that defines a unique 2-valued model, denoted Stratified (π), as discussed in Section 2.
Theorem 5 . For a program π with stratified negation and in which all predicates are certain,
Founded (π) = Stratified (π).

10

First-order logic. The next theorem relates constraint models with the interpretation of a program as a set of formulas in first-order logic; recall that the definition of a model of a program is
based on that interpretation.
Theorem 6 . For a program π in which all predicates are uncertain and not complete, the constraint
models of π are exactly the 2-valued models of π.
Fitting semantics. Fitting [Fit85] defines an interpretation to be a model of a program iff it satisfies a formula we denote CCmpl (π), which is Fitting’s 3-valued-logic version of the Clark completion
of π [Cla87]. Briefly, CCmpl (π) = CCmpl D (π) ∧ CCmpl U (π), where CCmpl D (π) is the conjunction
of formulas corresponding to the combined rules introduced by Combine except with ← replaced
with ∼
= (which is called “complete equivalence” and means “same truth value”), and CCmpl U (π) is
the conjunction of formulas stating that predicates not used in any fact or the conclusion of any
rule are false for all arguments. The Fitting model of a program π, denoted Fitting (π), is the least
model of CCmpl (π) [Fit85].
Theorem 7 . For a program π in which all extensional predicates are certain, and all intensional
predicates are uncertain and complete, Founded (π) = Fitting(π).
Founded semantics for some declarations is less defined than or equal to Fitting semantics, as
stated in the following theorem. A simple program π6 for which the inclusion is strict, as in part
(b) of the theorem, is program 6 in Table 2, which has only one rule q ← p, with both predicates
uncertain and complete. Founded (π6 ) = ∅ and Fitting (π6 ) = {p, q}.
Theorem 8 . (a) For a program π in which all intensional predicates are uncertain and complete,
Founded (π) ⊆ Fitting (π). (b) If, furthermore, some extensional predicate is uncertain, and some
positive literal p for some uncertain extensional predicate does not appear in π, then Founded (π) ⊂
Fitting(π).
Founded semantics for default declarations is at least as defined as Fitting semantics, as stated
in the following theorem. A simple program π3 for which the inclusion is strict, as in part (b)
of the theorem, is program 3 in Table 2, which has only one rule q ← q. Fitting (π3 ) = ∅ and
Founded (π3 ) = {¬ q}.
Theorem 9 . (a) For a program π in which all predicates have default declarations as certain or
uncertain and complete or not, Fitting(π) ⊆ Founded (π). (b) If, furthermore, Fitting(π) is not
2-valued for some certain intensional predicate P , then Fitting(π) ⊂ Founded (π).
Well-founded semantics. The well-founded model of a program π, denoted WFS (π), is the least
fixed point of a monotone operator Wπ on interpretations, defined as follows [VRS91]. A set U of
atoms of a program π is an unfounded set of π with respect to an interpretation I of π iff, for each
atom A in U , for each ground instance R of a rule of π with conclusion A, either (1) some hypothesis
of R is false in I or (2) some positive hypothesis of R is in U . Intuitively, the atoms in U can be set
to false, because each rule R whose conclusion is in U either has a hypothesis already known to be
false or has a hypothesis in U (which will be set to false). Let Uπ (I) be the greatest unfounded set of
program π with respect to interpretation I. For a set S of atoms, let ¬ · S denote the set containing
the negations of those atoms. Wπ is defined by Wπ (I) = Tπ (I) ∪ ¬ · Uπ (I). The well-founded model
WFS (π) satisfies CCmpl (π), so Fitting(π) ⊆ WFS (π) for all programs π [VRS91].
Theorem 10 . For every program π, Founded (π) ⊆ WFS (π).
One might conjecture that Founded (π) = WFS (π) for propositional programs. However, this is
false, as program 8 in Table 2 in Appendix A shows.

11

Supported models. Supported model semantics of a logic program is a set of 2-valued models.
An interpretation I is a supported model of π if I is 2-valued and I is a fixed point of the onestep derivability operator Tπ [ABW88]. Let Supported (π) denote the set of supported models of
π. Supported models, unlike Fitting semantics and WFS, allow atoms to be set to true when they
have circular positive dependency.
The following three theorems relating constraint semantics with supported model semantics are
analogous to the three theorems relating founded semantics with Fitting semantics. The inclusion
in Theorem 12 is strict for the program π6 described above. Supported (π6 ) = {{¬ p, ¬ q}} and
Constraint (π6 ) = {{p, q}, {¬ p, ¬ q}}. The inclusion in Theorem 13 is strict for the program π3
described above. Constraint (π3 ) = {{¬ q}} and Supported (π6 ) = {{q}, {¬ q}}.
Theorem 11 . For a program π in which all extensional predicates are certain, and all intensional
predicates are uncertain and complete, Supported (π) = Constraint (π).
Theorem 12 . For a program π in which all intensional predicates are uncertain and complete,
Supported (π) ⊆ Constraint (π).
Theorem 13 . For a program π in which all predicates have default declarations as certain or
uncertain and complete or not, Constraint (π) ⊆ Supported (π).
Stable models. Gelfond and Lifschitz define stable model semantics (SMS) of logic programs
[GL88]. They define the stable models of a program π to be the 2-valued interpretations of π that
are fixed points of a particular transformation. Van Gelder et al. proved that the stable models
of π are exactly the 2-valued fixed points of the operator Wπ described above [VRS91, Theorem
5.4]. Let SMS (π) denote the set of stable models of π. The inclusion in Theorem 14 is strict for
program 7 in Table 2, denoted π7 , which has two rules q ← ¬ q and q ← q. SMS (π7 ) = ∅ and
Constraint (π7 ) = {q}.
Theorem 14 . For a program π in which all predicates have default declarations as certain or
uncertain, SMS (π) ⊆ Constraint (π).
Example. For the win example with default declarations, Fitting semantics and WFS are the
same as founded semantics in Section 4, and supported model semantics and SMS are the same as
constraint semantics in Section 4. Additional examples can be found in Appendix B.


7

Computational complexity and extensions

Computing founded semantics and constraint semantics.
Theorem 15 . Computing founded semantics is linear time in the size of the ground program.
Proof.
First ground all given rules, using any grounding. Then add completion rules, if
any, by adding an inverse rule for each group of the grounded given rules that have the same
conclusion, yielding ground completion rules of the same asymptotic size as the grounded given
rules. Now compute the least fixed point for each SCC of the resulting ground rules using a
previous method [LS09]: introduce a new intermediate predicate and rule for each conjunction and
disjunction in the rules, yielding a new set of rules of the same asymptotic size; each resulting
rule incurs at most one rule firing, because there are no variables in the rule, and each firing takes
worst-case O(1) time. Thus, the total time is worst-case linear in the size of all ground rules and of
the grounded given rules.

The size of the ground program is polynomial in the size n of input data, i.e., the given facts,
because each variable in each rule can be instantiated at most O(n) times (because the domain size

12

is at most n), and there is a fixed number of variables in each rule, and a fixed size of the given rules.
Precisely, the size of the ground program is in the worst case O(nk × r), where k is the maximum
number of variables in a rule, and r is the size of the given rules.
Computing constraint semantics may take exponential time in the size of the input data, because
in the worse case, all assertions of all predicates may have U values in founded semantics, and there is
an exponential number of combinations of T and F values of all assertions, where each combination
may be checked for whether it satisfies the constraints imposed by all rules.
These complexity analyses also apply to the extensions below except that computing founded
semantics with closed predicates may take quadratic time in the size of the ground program, because
of repeated computation of founded semantics and self-false assertions.
Closed predicate assumption. We can extend the language to support declaration of uncertain
complete predicates as closed. Informally, this means that an atom A of the predicate is false
in an interpretation I, called self-false in I, if every ground instance of rules that concludes A,
or recursively concludes some hypothesis of that rule instance, has a hypothesis that is false or,
recursively, is self-false in I. Self-false atoms are elements of unfounded sets.
Formally, SelfFalse π (I), the set of self-false atoms of program π with respect to interpretation
I, is defined in the same way as the greatest unfounded set of π with respect to I, except replacing
“some positive hypothesis of R is in U ” with “some positive hypothesis of R for a closed predicate
is in U ”. The founded semantics of this extended language is defined by repeatedly computing
the semantics as per Section 4 and then setting self-false atoms to false, until a least fixed point
is reached. Formally, the founded semantics is FoundedClosed (π) = LFP (Fπ ), where Fπ (I) =
Founded (π ∪ I) ∪ ¬ · SelfFalse π (Founded (π ∪ I)).
The constraint semantics for this extended language includes only interpretations containing
the negative literals required by the closed declarations. A constraint model of a program π with
closed declarations is a consistent 2-valued interpretation M such that M is a model of Cmpl (π),
FoundedClosed (π) ⊆ M , and ¬ · SelfFalse π (M ) ⊆ M . Let ConstraintClosed (π) denote the set of
constraint models of π.
The next theorem states that changing predicate declarations from uncertain, complete, and
closed to certain, or vice versa, preserves founded and constraint semantics. Theorem 3 implies that
this change needs to be made for all predicates in an SCC.
Theorem 16 . Let π be a program. Let S be an SCC in its dependence graph containing only
predicates that are uncertain, complete, and closed and that can be declared certain, i.e., all SCCs
that precede S in dependency order contain certain predicates, and predicates in S do not have
circular negative dependency. Let π ′ be the program obtained from π by changing the declarations
of predicates in S from uncertain to certain. Then FoundedClosed (π) = FoundedClosed (π ′ ) and
ConstraintClosed (π) = ConstraintClosed (π ′ ).
Theorem 17 . For a program π in which every uncertain predicate is complete and closed,
FoundedClosed (π) = WFS (π).
Theorem 18 . For a program π in which every uncertain predicate is complete and closed,
ConstraintClosed (π) = SMS (π).
Note, however, that founded semantics for default declarations (certain when possible and complete otherwise) allows the number of repetitions for computing self-false atoms to be greatly reduced, even to zero, compared with WFS that does repeated computation of unfounded sets.
In all examples we have found in the literature, and all natural examples we have been able
to think of, founded semantics for default declarations, without closed predicate assumption, infers
13

the same result as WFS. While founded semantics computes a single least fixed point without the
outer repetition and is worst-case linear time, WFS computes an alternating fixed point or iterated
fixed point and is worst-case quadratic. In fact, we have not found any natural example showing
that an actual quadratic-time alternating or iterated fixed-point for computing WFS is needed.1
Unrestricted existential and universal quantifications in hypotheses. We extend the language to allow unrestricted combinations of existential and universal quantifications as well as
negation, conjunction, and disjunction in hypotheses. The domain of each quantified variable is the
set of all constants in the program.
Example. For the win example, the following two rules may be given instead:
win(x) ← ∃ y | move(x,y) ∧ lose(y)
lose(x) ← ∀ y | ¬ move(x,y) ∨ win(y)


The semantics in Section 4 is easily extended to accommodate this extension: these constructs
simply need to be interpreted, using their 3-valued logic semantics [Fit85], when defining one-step
derivability. Theorems 1–4 hold for this extended language. The other semantics discussed above
are not defined for this extension, so we do not have theorems relating to them.
Negation in facts and conclusions. We extend the language to allow negation in given facts
and in conclusions of given rules; such facts and rules are said to be negative. The Yale shooting
example in Appendix B is a simple example.
The definition of founded semantics applies directly to this extension, because it already introduces and handles negative rules, and it already infers and handles negative facts. Note that
Combine combines only positive facts and positive rules to form combined rules; negative facts and
negative rules are copied unchanged into the completed program.
With this extension, a program and hence its founded model may be inconsistent; for example,
a program could contain or imply p and ¬p. Thus, Theorem 1 does not hold for such programs.
When the founded model is inconsistent, the inconsistent literals in it can easily be reported to the
user. When the founded model is consistent, the definition of constraint semantics applies directly,
and Theorems 2–4 hold. The other semantics discussed above are not defined for this extended
language, so we do not have theorems relating to them.

8

Related work and conclusion

There is a large literature on logic language semantics. Several overview articles [AB94, Prz94,
RU95, Fit02, Tru17] give a good sense of the challenges when there are unrestricted negation. We
discuss major related work.
Clark [Cla87] describes completion of logic programs to give a semantics for negation as failure.
Numerous others, e.g., [LT84, ST84, JLM86, Cha88, FRTW88, Stu91], describe similar additions.
Fitting [Fit85] presents a semantics, called Fitting semantics or Kripke-Kleene semantics, that aims
to give a least 3-valued model. Apt et al. [ABW88] defines supported model semantics, which is a set
of 2-valued models; the models correspond to extensions of the Fitting model. Apt et al. [ABW88]
1
Even a contrived example that demonstrates the worst-case quadratic-time computation of WFS has been challenging to find. For example, the quadratic-time example in [Zuk01] turns out to be linear in XSB; after significant
effort between us and Warren, we found a much more sophisticated one that appears to work, but a remaining bug
in XSB makes the correctness of its computation unclear.

14

and Van Gelder [VG89] introduce stratified semantics. WFS [VRS91, VG93] also gives a 3-valued
model but aims to maximize false values. SMS [GL88] also gives a set of 2-valued models and
aims to maximize false values. Other formalisms and semantics include partial stable models, also
called stationary models [Prz94], and FO(ID), for first-order logic with inductive definitions [DT08].
There are also many studies that relate different semantics, e.g. [Dun92].
Our founded semantics, which extends to constraint semantics, is unique in that it allows predicates to be specified as certain or uncertain, as complete or not, and as closed or not. These choices
clearly and explicitly capture the different assumptions one can have about the predicates, rules,
and reasoning, including the well-known closed-world assumption vs open-world assumption—i.e.,
whether or not all rules and facts about a predicate are given in the program—and allow both to
co-exist naturally. These choices make our new semantics more expressive and intuitive. Instead of
using many separate semantics, one just need to make the assumptions explicit; the same underlying
logic is used for inference. In this way, founded semantics and constraint semantics unify the core
of different semantics.
In addition, founded semantics and constraint semantics are completely declarative and easy to
understand, as a least fixed point and as constraint satisfaction, respectively. Our default declarations without closed predicates lead to the same semantics as WFS and SMS for all natural examples
we have found. Additionally, founded semantics without closed predicates can be computed in linear
time in the size of the ground program, as opposed to quadratic time for WFS.
There are many directions for future study, including additional relationships with prior semantics, further extensions, efficient implementations, and many applications.

References
[AB94]

Krzysztof R. Apt and Roland N. Bol. Logic programming and negation: A survey. Journal of
Logic Programming, 19:9–71, 1994.

[ABW88]

Krzysztof R. Apt, Howard A. Blair, and Adrian Walker. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming, pages 89–148. Morgan
Kaufman, 1988.

[AHV95]

Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases: The Logical Level.
Addison-Wesley, 1995.

[CGT90]

Stefano Ceri, Georg Gottlob, and Letizia Tanca. Logic Programming and Databases. Springer,
1990.
David Chan. Constructive negation based on the completed database. In Proc. of the 5th Intl.
Conf. and Symp. on Logic Programming, pages 111–125. MIT Press, 1988.

[Cha88]
[CKW93]

Weidong Chen, Michael Kifer, and David S. Warren. HiLog: A foundation for higher-order logic
programming. Journal of Logic Programming, 15(3):187–230, 1993.

[Cla87]

Keith L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases,
pages 293–322. Plenum Press, Apr. 1987.

[DT08]

M. Denecker and E. Ternovska. A logic of nonmonotone inductive definitions. ACM Transactions
on Computational Logic, 9(2):14, 2008.

[Dun92]

Phan Minh Dung. On the relations between stable and well-founded semantics of logic programs.
Theoretical Computer Science, 105(1):7–25, 1992.

[Fit85]

Melvin Fitting. A Kripke-Kleene semantics for logic programs. Journal of Logic Programming,
2(4):295–312, 1985.

[Fit02]

Melvin Fitting. Fixpoint semantics for logic programming: A survey. Theoretical Computer
Science, 278(1):25–51, 2002.

15

[FRTW88] Norman Y. Foo, Anand S. Rao, Andrew Taylor, and Adrian Walker. Deduced relevant types and
constructive negation. In Proc. of the 5th Intl. Conf. and Symp. on Logic Programming, pages
126–139, 1988.
[GL88]
[JLM86]
[LS09]

Michael Gelfond and Vladimir Lifschitz. The stable model semantics for logic programming.
In Proc. of the 5th Intl. Conf. and Symp. on Logic Programming, pages 1070–1080. MIT Press,
1988.
Joxan Jaffar, Jean-Louis Lassez, and Maher J. Maher. Some issues and trends in the semantics of
logic programming. In Proc. on 3rd Intl. Conf. on Logic Programming, pages 223–241. Springer,
1986.
Yanhong A. Liu and Scott D. Stoller. From Datalog rules to efficient programs with time and
space guarantees. ACM Transactions on Programming Languages and Systems, 31(6):1–38, 2009.

[LT84]

John W. Lloyd and Rodney W. Topor. Making Prolog more expressive. Journal of Logic Programming, 1(3):225–240, 1984.

[Prz94]

T.C. Przymusinski. Well-founded and stationary models of logic programs. Annals of Mathematics and Artificial Intelligence, 12(3):141–187, 1994.

[RU95]

Raghu Ramakrishnan and Jeffrey D Ullman. A survey of deductive database systems. Journal
of Logic Programming, 23(2):125–149, 1995.

[ST84]

Taisuke Sato and Hisao Tamaki. Transformational logic program synthesis. In Proceedings of
the International Conference on Fifth Generation Computer Systems, pages 195–201, 1984.

[Stu91]

Peter J Stuckey. Constructive negation for constraint logic programming. In Proceedings of the
6th Annual IEEE Symposium on Logic in Computer Science, pages 328–339, 1991.

[Tru17]

Mirek Truszczynski. An introduction to the stable and the well-founded semantics of logic programs. In Michael Kifer and Yanhong A. Liu, editors, Declarative Logic Programming: Theory,
Systems, and Applications. ACM and Morgan & Claypool, 2017. Expected.

[VG89]

Allen Van Gelder. Negation as failure using tight derivations for general logic programs. Journal
of Logic Programming, 6(1):109–133, 1989.

[VG93]

Allen Van Gelder. The alternating fixpoint of logic programs with negation. Journal of Computer
and System Sciences, 47(1):185–221, 1993.

[VRS91]

Allen Van Gelder, Kenneth Ross, and John S. Schlipf. The well-founded semantics for general
logic programs. Journal of the ACM, 38(3):620–650, 1991.

[Zuk01]

Ulrich Zukowski. Flexible Computation of the Well-Founded Semantics of Normal Logic Programs. PhD thesis, Faculty of Computer Science and Mathematics, University of Passau, 2001.

A

Comparison of semantics for well-known small examples and
more

Table 2 shows well-known example rules and more for tricky boundary cases in the semantics, where
all uncertain predicates that are in a conclusion are declared complete, but not closed, and shows
different semantics for them.
• Programs 1 and 2 contain only negative cycles. All three of Founded, WFS, and Fitting agree.
All three of Constraint, SMS, and Supported agree.
• Programs 3 and 4 contain only positive cycles. Founded for certain agrees with WFS; Founded
for uncertain agrees with Fitting. Constraint for certain agrees with SMS; Constraint for
uncertain agrees with Supported.
• Programs 5 and 6 contain no cycles. Founded for certain agrees with WFS and Fitting;
Founded for uncertain has more undefined. Constraint for certain agrees with SMS and
Supported; Constraint for uncertain has more models.
16

Program Founded (not closed)
uncertain certain
1 q←¬q
q←¬p
2
p←¬q
3 q←q
q←p
4
p←q
5 q←¬p
6 q←p
q←¬q
q←q
q←¬q
8
∧q
7

WFS

{q}

–

{q}

Fitting
(Kripke
-Kleene)
{q}

{p, q}

–

{p, q}

{q}

{q}

{p, q}

Constraint (not closed)
uncertain
certain

SMS

Supported

no model

–

no model

no model

{p, q}

{p, q},{p, q}

–

{p, q},{p, q}

{p, q},{p, q}

{q}

{q}

{q},{q}

{q}

{q}

{q},{q}

{p, q}

{p, q}

{p, q}

{p, q},{p, q}

{p, q}

{p, q}

{p, q},{p, q}

{p, q}
{p, q}

{p, q}
{p, q}

{p, q}
{p, q}

{p, q}
{p, q}

{p, q},{p, q}
{p, q},{p, q}

{p, q}
{p, q}

{p, q}
{p, q}

{p, q}
{p, q}

{q}

–

{q}

{q}

{q}

–

no model

{q}

{q}

–

{q}

{q}

{q}

–

{q}

{q}

Table 2: Different semantics for programs where all uncertain predicates that are in a conclusion
are declared complete, but not closed. “uncertain” means all predicates in the program are declared
uncertain. “certain” means all predicates in the program that can be declared certain are declared
certain; “–” means no predicates can be declared certain, so the semantics is the same as “uncertain”.
p, p and p mean p is T , F , and U , respectively.
• Programs 7 and 8 contain both negative and positive cycles. For program 7 where ¬ q and
q are disjunctive, all three of Founded WFS, and Fitting agree; Constraint and Supported
agree, but SMS has no model. For program 8 where ¬ q and q are conjunctive, Founded and
Fitting agree, but WFS has q being F ; all three of Constraint, SMS, and Supported agree.
For all 8 programs, with default complete but not closed predicates, we have the following:
• If all predicates are the default certain or uncertain, then Founded agrees with WFS, and
Constraint agrees with SMS, with one exception for each:
(1) Program 7 concludes q whether q is F or T , so SMS having no model is an extreme outlier
among all 6 semantics and is not consistent with common sense.
(2) Program 8 concludes q if q is F and T , so Founded semantics with q being U is imprecise,
but Constraint has q being F . WFS has q being F because it uses F for ignorance.
• If predicates not in any conclusion are certain (not shown in Table 2 but only needed for q
in programs 5 and 6), and other predicates are uncertain, then Founded equals Fitting, and
Constraint equals Supported, as captured in Theorems 7 and 11, respectively.
• If all predicates are uncertain, then Founded has all values being U , capturing the well-known
unclear situations in all these programs, and Constraint gives all different models except for
programs 2 and 5, and programs 4 and 6, which are pair-wise equivalent under completion,
capturing exactly the differences among all these programs.
Finally, if all predicates in these programs are not complete, then Founded and Constraint are the
same as in Table 2 except that Constraint for uncertain becomes equivalent to truth values in firstorder logic: programs 1 and 8 have an additional model, {q}, program 6 has an additional model,
{p, q}, and programs 2 and 5 have an additional model, {p,q}.

17

B

Additional examples

We discuss the semantics of some well-known examples.
Graph reachability. A source vertex x is represented by a fact source(x). An edge from a
vertex x to a vertex y is represented by a fact edge(x,y). The following two rules capture graph
reachability, i.e., the set of vertices reachable from source vertices by following edges.
reach(x) ← source(x)
reach(y) ← edge(x,y) ∧ reach(x)

In the dependency graph, each predicate is in a separate SCC, and the SCC for reach is ordered
after the other two. There is no negation in this program.
With the default declaration of predicates being certain, no completion rules are added. The
least fixed point computation for founded semantics infers reach to be T for all vertices that are
source vertices or are reachable from source vertices by following edges, as desired. For the remaining
vertices, reach is F . This is the same as WFS.
If reach is declared uncertain and complete, but not closed, then after completion, we obtain
reach(x) ← source(x) ∨
(∃ y | (edge(y,x) ∧ reach(y)))
n.reach(x) ← n.source(x) ∧
(∀ y | (n.edge(y,x) ∨ n.reach(y)))

The least fixed point computation for founded semantics infers reach to be T for all reachable
vertices as when predicates are certain, and infers reach to be F for all vertices that are not source
vertices and that have no in-coming edge at all or have in-coming edges only from vertices for which
reach is F . For the remaining vertices, i.e., those that are not reachable from the source vertices
but are in cycles of edges, reach is U . This is the same as in Fitting semantics.
Russell’s paradox. Russell’s paradox is illustrated as the barber paradox. The barber is a man
who shaves all those men, and those men only, who do not shave themselves, as specified below.
The question is: Does the barber shave himself? That is: What is the value of shave(’barber’,
’barber’)?
shave(’barber’,x) ← man(x) ∧ ¬ shave(x,x)
man(’barber’)

Since shave is defined transitively using its own negation, it is uncertain. With the default
declaration that shave is complete, but not closed, the completion step adds the rule
¬ shave(’barber’,x) ← ¬ man(x) ∨ shave(x,x)

The completed program, after eliminating negation, is
shave(’barber’,x) ← man(x) ∧ n.shave(x,x)
man(’barber’)
n.shave(’barber’,x) ← n.man(x) ∨ shave(x,x)

The least fixed point computation for founded semantics infers no T or F facts of shave, so
shave(’barber’,’barber’) is U . Constraint semantics has no model. These results correspond
to WFS and SMS, respectively. All confirm the paradox.
Additionally, if there are other men besides the barber, then founded semantics will also infer
shave(’barber’,x) for all man x except ’barber’ to be T , and shave(x,y) for all man x except
’barber’ and for all man y to be F , confirming the paradox that only shave(’barber’,’barber’)
is U . Constraint semantics has no model. These results again correspond to WFS and SMS,
respectively.
18

Even numbers. In this example, even numbers are defined by the predicate even, and natural
numbers in order are given using the predicate succ.
even(n) ← succ(m,n) ∧ ¬ even(m)
even(0)
succ(0,1)
succ(1,2)
succ(2,3)

With default declarations, founded semantics infers that even(1) is F , even(2) is T , and even(3) is
F . Constraint semantics is the same. These results are the same as WFS and SMS, respectively.
Yale shooting. This example is about whether a turkey is alive, based on some facts and rules,
given below, about whether and when the gun is loaded. It uses the extension that allows negative
facts and negative conclusions.
alive(0)
¬ loaded(0)
loaded(1) ← T
¬ alive(3) ← loaded(2)

Both predicates are declared uncertain and not complete. In the dependency graph, there are two
SCCs: one with loaded, one with alive, and the former is ordered before the latter. Founded
semantics infers that loaded(0) is F , loaded(1) is T , loaded(2) and loaded(3) are U , alive(0) is
T , and alive(1), alive(2), and alive(3) are U . Constraint semantics has multiple models, some
containing that loaded(2) is T and alive(3) is F , and some containing that loaded(2) is F and
alive(3) is T . Both confirm the well-known outcome.
Variant of Yale shooting. This is a variant of the Yale shooting problem, copied from [VRS91]:
noise(T) ← loaded(T) ∧ shoots(T).
loaded(0).
loaded(T) ← succ(S,T) ∧ loaded(S) ∧ ¬ shoots(S).
shoots(T) ← triggers(T).
triggers(1).
succ(0,1).

There is no circular negative dependency, so all predicates are certain by default, and no completion
rules are added. Founded semantics and constraint semantics both yield: trigger(1), ¬ trigger(0),
shoots(1), ¬ shoots(0), noise(1), ¬ noise(0), loaded(1), and loaded(0). This is the same as WFS,
Fitting semantics, SMS, and supported models.

C

Proofs

Proof of Theorem 1. First we show the founded model is consistent. A given program cannot
contain negative facts or negative conclusions, so all negative literals in Founded (π) are added
by the construction. For a predicate declared uncertain and not complete, no negative literals
are added. For a predicate P declared uncertain and complete, consistency follows from the fact
that the only rule defining n.P in Cmpl (π) is the inverse of the only rule defining P in Cmpl (π).
The body of the former rule is the negation of the body B of the latter rule. Monotonicity of
TIi−1 ∪Proj (NameNeg (Cmpl (π)),Si ) implies that the value of a ground instance of B cannot change from
19

true to false, or vice versa, during the fixed point calculation for the SCC S containing P . Using this
observation, it is easy to show by induction on the number of iterations of the fixed point calculation
for S that an atom for P and its negation cannot both be added to the interpretation. For a certain
predicate, consistency follows from the fact that AddNeg adds only literals whose complement is
not in the interpretation. Constraint models are consistent by definition.

Proof of Theorem 2.
First we show that Founded (π) is a model of Cmpl (π). Founded (π)
contains all facts in π, because each fact in π is either merged into a combined rule in Cmpl (π) or
copied unchanged into Cmpl (π), and in either case is added to the founded model by the LFP for
some SCC. Consider a rule C ← B in Cmpl (π) with predicate Q in the conclusion C. Note that
C may be a positive or negative literal. If the body B becomes true before or in the LFP for the
SCC S containing Q, then the corresponding disjunct in the combined rule defining Q becomes true
before or in that LFP, so the conclusion C is added to the interpretation by that LFP, so the rule
is satisfied. It remains to show that B could not become true after that LFP. B cannot become
true during processing of a subsequent SCC, because SCCs are processed in dependency order, so
subsequent SCCs do not contain predicates in B. We prove by contradiction that B cannot become
true in AddNeg for S, i.e., we suppose B becomes true in AddNeg for S and show a contradiction.
AddNeg for S adds only negative literals for certain predicates in S, so B must contain such a literal,
say ¬P (. . .). P and Q are in the same SCC S, so P must be defined, directly or indirectly, in terms
of Q. Since P is certain and is defined in terms of Q, Q must be certain. Since Q and P are defined
in the same SCC S, and Q depends negatively on P , Q has a circular negative dependency, so Q
must be uncertain, a contradiction.
Constraint models are 2-valued models of Cmpl (π) by definition.
Any model of Cmpl (π) is also a model of π, because π is logically equivalent to the subset of
Cmpl (π) obtained by removing the completion rules added by AddInv .

Proof of Theorem 3.
It suffices to show that, if some predicate in S is uncertain, then all
predicates in S are uncertain. Suppose S contains an uncertain predicate P , and let Q be another
predicate in S. Q is defined directly or indirectly in terms of predicate P , and P is uncertain, so Q
must be uncertain.

Proof of Theorem 4.
The proof is based on a straightforward correspondence between the
constructions of founded semantics of π and Merge S (π).
Note that:
• All predicates in S are certain, or all of them are uncertain, by Theorem 3.
• There is a 1-to-1 correspondence between the set of disjuncts in the bodies of the rules for
predicates in S in Cmpl (π) and the set of disjuncts in the body of the rule for holds in
Cmpl (Merge S (π)).
• If predicates in S are uncertain and complete, there is a 1-to-1 correspondence between the
set of conjuncts in the bodies of the completion rules for predicates in S in Cmpl (π) and the
set of conjuncts in the body of the completion rule for holds in Cmpl (Merge S (π)).
Based on these observations, it is straightforward to show that:
• For each predicate P not in S, each atom A for P or n.P is derivable in the semantics for π
iff A is derivable in the semantics for Merge S (π).
• In the LFP for the SCC containing S, for each predicate P in S, an atom A for P is derivable using a disjunct of the rule for P in Cmpl (π) iff MergeAtom S (A) is derivable using the
corresponding disjunct of the rule for holds in Cmpl (Merge S (π)).
20

• In the LFP for the SCC containing S, for each uncertain complete predicate P in S, an atom
A for n.P is derivable using the completion rule for P in π iff MergeAtom S (A) is derivable
using the corresponding conjuncts in the completion rule for holds in Merge S (π) (the other
conjuncts in the completion rule for holds have the form v 6= "Q" ∨ · · · and hence are true
when considering derivation of atoms of the form n.holds("P ", . . .)).
• In AddNeg for the SCC containing S, for each certain predicate P in S, an atom A for n.P is
inferred in the semantics for π iff MergeAtom S (A) is inferred in the semantics for Merge S (π).

Proof of Theorem 5.
For certain predicates, the program completion Cmpl has no effect,
and LFPbySCC is essentially the same as the definition of stratified semantics, except using SCCs
in the dependency graph instead of strata. The SCCs used in founded semantics subdivide the
strata used in stratified semantics; intuitively, this is because predicates are put in different SCCs
whenever possible, while predicates are put in different strata only when necessary. This subdivision
of strata does not affect the result of LFPbySCC , so founded semantics is equivalent to the stratified
semantics.

Proof of Theorem 6. Observe that, for a program π satisfying the hypotheses of the theorem,
Cmpl (π) is logically equivalent to π. Every constraint model is a 2-valued model of Cmpl (π) and
hence a 2-valued model of π. Consider a 2-valued model M of π. Since π satisfies the hypotheses
of the theorem, Founded (π) contains only positive literals, added by the LFPs in LFPbySCC . The
LFPs add a positive literal to Founded (π) only if that literal is implied by the facts and rules in π
and therefore holds in all 2-valued models of π. Therefore, Founded (π) ⊆ M . M satisfies π and
hence, by the above observation, also Cmpl (π). Thus, M is a constraint model of π.

Proof of Theorem 7. Consider an intensional predicate P . By assumption, P is uncertain and
complete. It is straightforward to show that the LFP for the SCC containing P using the combined
rule for P in Cmpl (π), of the form C ← B, and its inverse, of the form ¬C ← ¬B, is equivalent to
satisfying the conjunct for P in CCmpl D (π), of the form C ∼
= B. The proof for the forward direction
( =⇒ ) of the equivalence is a case analysis on the truth value of the body B in Founded (π): (1) if
B is true, then the LFP uses the combined rule C ← B to infer C is true, so C ∼
= B holds; (2) if B
B
holds;
(3)
if B is undefined,
is false, then the LFP uses the inverse rule to infer C is false, so C ∼
=
∼
then neither rule applies and C is undefined, so C = B holds. Similarly, the proof for the reverse
direction (⇐) is a simple case analysis on the truth values of B and C (which are the same, since
C∼
= B by assumption).
Consider an extensional predicate P . By assumption, P is certain. Let S be the set of atoms
for P in π. It is easy to show that Founded (π) and Fitting (π) contain the atoms in S and contain
negative literals for P for all other arguments.

Proof of Theorem 8. (a) This follows from Theorem 7 and the observation that, if π satisfies the
premises of Theorem 7, and π ′ is obtained from π by changing the declarations of some extensional
predicates from certain to uncertain, then Founded (π ′ ) ⊆ Founded (π); intuitively, fewer assumptions
are made about uncertain predicates, so Founded (π ′ ) contains fewer conclusions. (b) This follows
from part (a) and the observation that p is undefined in Founded (π), and p is false in Fitting(π)
(i.e., Fitting(π) contains ¬p), so the inclusion relation is strict.

Proof of Theorem 9. (a) This follows from Theorem 7, the differences between the declarations
assumed in Theorem 7 and the default declarations, and the effect of those differences on the founded
21

model. It is easy to show that the default declarations can be obtained from the declarations
assumed in Theorem 7 by changing the declarations of some intensional predicates from uncertain
and complete to certain. Let P be such a predicate. This change does not affect the set S of positive
literals derived for P , because the combined rule for P is equivalent to the original rules and facts
for P . This change can only preserve or increase the set of negative literals derived for P , because
AddNeg derives all negative literals for P that can be derived while preserving consistency of the
interpretation (in particular, negative literals for all arguments of P not in S).
(b) This follows from the proof of part (a) and the observation that the additional premise for
part (b) implies there is a literal p for P that is undefined in Fitting(π) and defined (i.e., true or
false) in Founded (π) (because Founded (π) is 2-valued for P ), so the inclusion is strict.

Proof of Theorem 10.
We prove an invariant that, at each step during the construction of
Founded (π), the current approximation I to Founded (π) satisfies I ⊆ WFS (π). It is straightforward
to show, using the induction hypothesis, that literals added to I by the LFPs in LFPbySCC are
in WFS (π). Consider a literal p added by a combined rule C ← B. This implies B is true in
I. By the induction hypothesis, I ⊆ WFS (π), so B is true in WFS (π). Using the rule in π
corresponding to a disjunct in B that is true in I, we conclude p ∈ Tπ (WFS (π)). The definition
of WFS (π) implies WFS (π) is closed under Tπ , so p ∈ WFS (π). Consider a literal ¬p added by a
combined rule ¬C ← ¬B. All of the disjuncts in the negation normal form of B are true in I, so
the bodies of all rules in π that derive p are false in I and, by the induction hypothesis, are false in
WFS (π), so p ∈ Uπ (WFS (π)). The definition of WFS (π) implies WFS (π) is closed under ¬ · Uπ ,
so ¬p ∈ WFS (π).
It remains to show that negative literals added to I by AddNeg are in WFS (π). Consider an
SCC S in the dependency graph. Let NS be the set of atoms whose negations are added to I by
AddNeg for S. Let IS denote the interpretation produced by the LFP for S. Since Uπ is monotone,
it suffices to show that NS is an unfounded set for π with respect to IS , i.e., for each atom A in
NS , for each ground instance A ← B of a rule of π with conclusion A, either (1) some hypothesis
in B is false in IS or (2) some positive hypothesis in B is in NS . We use a case analysis on the
truth value of B in IS . B cannot be true in IS , because if it were, A would be added to IS by the
LFP and would not be in NS . If B is false in IS , then case (1) holds. Suppose B is undefined in IS .
This implies that at least one hypothesis H in B is undefined in IS . Let Q be the predicate in A,
and let P be the predicate in H. AddNeg adds literals only for certain predicates, so Q is certain.
Q depends on P , so P must be certain, and P must be in S or a previous SCC. If P were in a
previous SCC, then IS would be 2-valued for P , and H would be T or F in IS , a contradiction, so
P is in S. Since P is in S, and H is undefined in IS , AddNeg adds ¬H to IS , i.e., H is in NS . Q is
certain, so Q does not have circular negative dependency; therefore, since P and Q are both in S,
H must be a positive hypothesis. Thus, case (2) holds.

Proof of Theorem 11. Let M ∈ Supported (π). We show M ∈ Constraint (π), i.e., Founded (π) ⊆
M and M is a 2-valued model of π. Theorem 15 of [ABW88] shows that an interpretation I is a
supported model of π iff I is a 2-valued model of CCmpl (π) . Therefore, M is a model of CCmpl (π).
Theorem 7 implies that Founded (π) is the least model of CCmpl (π), so Founded (π) ⊆ M . For each
intensional predicate P (hence P is uncertain and complete, by assumption), the conjunction of the
combined rule for P and its inverse in Cmpl (π) is logically equivalent for 2-valued models to the
equivalence for P in CCmpl (π); this is a straightforward tautology in 2-valued logic. Thus, since
M is a model of CCmpl (π), it is also a model of Cmpl (π). Thus, M is a constraint model of π.
Let M ∈ Constraint (π). We show that M ∈ Supported (π). By definition, M is 2-valued, M
22

satisfies Cmpl (π), and Founded (π) ⊆ M . Note that Founded (π) ⊆ M implies Founded (π) and M
contain the same literals for all certain predicates. By Apt et al.’s theorem cited above, it suffices
to show that M is 2-valued and satisfies CCmpl (π). We show that the clause in CCmpl (π) for each
predicate P is satisfied, by case analysis on P . Case 1: P does not appear in any fact or conclusion.
Then P is extensional and hence certain, so AddNeg makes P false for all arguments in Founded (π)
and hence in M , so M satisfies the clause for P in CCmpl U (π). Case 2: P appears in some fact
or conclusion. Case 2.1: P is extensional, hence certain. Theorem 7 implies Founded (π) satisfies
CCmpl (π). Since Founded (π) and M contain the same literals for P , M satisfies the clause for P
in CCmpl D (π). Case 2.2: P is intensional, hence uncertain and complete. M satisfies CCmpl D (π),
which contains a combined rule of the form C ← B for P and the inverse rule ¬C ← ¬B. Since
M is 2-valued, the conjunction of those rules is equivalent to C ∼
= B, which is the clause for P in
CCmpl D (π).

Proof of Theorem 12. This theorem follows from Theorem 11, and the observation that, if π
satisfies the premises of Theorem 11, and π ′ is obtained from π by changing the declarations of some
extensional predicates from certain to uncertain, then Constraint (π) ⊆ Constraint (π ′ ). To prove
this, we analyze how the change in declarations affects Founded (π) and Cmpl (π), and then show
that the changes to Founded (π) and Cmpl (π) preserve or increase the set of constraint models. As
shown in the proof of Theorem 8, the founded model decreases, i.e., Founded (π ′ ) ⊆ Founded (π).
This may allow additional constraint models, because more models satisfy the requirement of being
a superset of the founded model. The effect on Cmpl (π) is to add completion rules for the predicates
whose declaration changed. This does not change the set of constraint models, because all constraint
models of π satisfy these completion rules. This follows from the lemma: For a program π and a
certain predicate P in π, every constraint model M of π satisfies the completion rule R for P (even
though this rule does not appear in Cmpl (π), because P is certain). To see this, first note that P
and hence all predicates on which it depends are certain, so all predicates used in R are certain,
so Founded (π) is 2-valued for those predicates, so Founded (π) and M contain the same literals for
those predicates, so M satisfies R iff Founded (π) satisfies R. To see that Founded (π) satisfies R, let
C ← B denote the combined rule for P , so R is ¬C ← ¬B, and note that Founded (π) contains a
positive literal for P for arguments for which B holds in Founded (π) and contains a negative literal
for P for all other arguments, and B is false for all of those other arguments, because Founded (π)
is 2-valued for all predicates used in B and hence for B.

Proof of Theorem 13.
This theorem follows from Theorem 11, the differences between the
declarations assumed in Theorem 11 and the default declarations, and the effect of those differences
on the constraint models. We analyze how the differences in declaration affect Founded (π) and
Cmpl (π), and then analyze how the changes to Founded (π) and Cmpl (π) affect the set of constraint
models. Specifically, we show that the set of constraint models is preserved or decreases and hence
that Constraint (π) ⊆ Supported (π).
The declarations assumed in Theorem 11 are the same as in Theorem 7. Recall from the proof
of Theorem 9 that the default declarations can be obtained from those declarations by changing
the declarations of some intensional predicates from uncertain and complete to certain. Let S be
the set of predicates whose declarations change. As discussed in the proof of Theorem 9, the effect
of these declaration changes on Founded (π) is to preserve or increase the set of negative literals for
predicates in S. The effect of these declaration changes on Cmpl (π) is to remove completion rules
for predicates in S.
Now consider the effects of these changes on the set of constraint models. Adding negative literals
23

to the founded model has the effect of decreasing the set of constraint models of the program, because
constraint models not containing those literals are eliminated, since each constraint model must be
a superset of the founded model. Removing from Cmpl (π) the completion rules for predicates in
S does not cause any further changes to the set of constraint models, because the interpretation of
predicates in S in the constraint models is now completely determined by the requirement that the
constraint models are supersets of the founded model, because the founded model is 2-valued for
predicates in S.

Proof of Theorem 14.
Let M ∈ SMS (π). We need to show M ∈ Constraint (π), i.e.,
Founded (π) ⊆ M and M is a 2-valued model of Cmpl (π). By Theorem 10, Founded (π) ⊆ WFS (π).
M is a fixed point of Wπ [VRS91, Theorem 5.4], so WFS (π) ⊆ M . By transitivity, Founded (π) ⊆ M .
It is easy to show that M is a 2-valued model of Cmpl (π) iff it is a 2-valued model of π and Cmpl N (π),
where Cmpl N (π) denotes the completion rules added by AddInv (“N” reflects the negative conclusions). Gelfond and Lifschitz proved that every stable model of π is a 2-valued model of π [GL88,
Theorem 1]. It remains to show that M is a model of Cmpl N (π). Let ¬P ← ¬H1 ∧ · · · ∧ ¬Hn be
a rule in Cmpl N (π). We need to show that, if M satisfies ¬H1 ∧ · · · ∧ ¬Hn , then M satisfies ¬P .
It suffices to show P ∈ Uπ (M ), because this implies ¬P ∈ M . The rules defining P in π have the
form P ← Hi , for i ∈ [1..n], and each Hi is false in M by assumption, so some conjunct in each Hi
is false in M , so by definition of unfounded set, P ∈ Uπ (M ).

Proof of Theorem 16. First, we show that FoundedClosed (π) is 2-valued for predicates in S.
Let RS be the set of all instances of combined rules and completion rules in Cmpl (π) for predicates
in S. Note that every positive literal and negative literal for every predicate in S appears as the
conclusion of at least one rule in G (this holds even if rules in π contain conclusions of the form
p(x,x) or p(x,0), due to the fresh variables and existential quantifiers introduced by Combine). Let
U be the set of atoms for predicates in S that are undefined in Founded (π). For each atom A in
U , since the predicate in A is complete and A is not T or F in Founded (π), (1) for every rule R in
RS with conclusion A, some hypothesis of R is F or U in Founded (π), and (2) for some rule R in
RS with conclusion A, some hypothesis of R is U in Founded (π). Since all predicates in SCCs that
precede S are certain, these undefined hypotheses must be atoms in U or their negations. Define a
dependence relation → on U by: B → A if some rule R in RS with conclusion A has an undefined
hypothesis that is B or ¬B. The previous observation implies that, for every A in U , there exists
B in U such that B → A. Since U is finite, this implies that every atom in U is in a →-cycle. Since
predicates in S do not have circular negative dependency, this implies that all hypotheses involved in
the cycle are positive. These observations, together with all predicates in S being close, imply that
the literals in every cycle, and hence every atom in U , is in SelfFalse π (Founded (π)). This implies
that FoundedClosed (π) contains the negations of all literals in U . Therefore, FoundedClosed (π) is
2-valued.
Next, we show that FoundedClosed (π) = FoundedClosed (π ′ ). For each predicate P in S, the two
programs contain equivalent rules for adding positive literals for P to the founded model, because the
combined rule for P in π is logically equivalent to the original rules for P in π, so FoundedClosed (π)
and FoundedClosed (π ′ ) contain the same positive literals for P . Since both models are 2-valued for
P , they also contain the same negative literals for P .
Finally, we show that ConstraintClosed (π) = ConstraintClosed (π ′ ). We consider the three
conditions in the definition of ConstraintClosed , in turn.
Consider the first condition, namely, FoundedClosed (π) ⊆ M . It is equivalent for the two
programs, because they have the same founded model.
24

Consider the second condition, namely, M satisfies Cmpl (π). It differs for the two programs
in that Cmpl (π) contains combined rules and completion rules for predicates in S, while Cmpl (π ′ )
contains the original rules in π for predicates in S. Since FoundedClosed (π) = FoundedClosed (π ′ ),
Theorem 1 implies FoundedClosed (π) is a model of Cmpl (π) and Cmpl (π ′ ). Since FoundedClosed (π)
is 2-valued for predicates in S and all predicates on which they depend, it is 2-valued for all predicates
used in those rules. Therefore, every M satisfying FoundedClosed (π) ⊆ M contains the same literals
as FoundedClosed (π) for all predicates used in those rules, so M satisfies Cmpl (π) and Cmpl (π ′ ).
Thus, the second condition is equivalent for the two programs.
Consider the third condition, namely, ¬ · SelfFalse π (M ) ⊆ M . FoundedClosed (π) is 2-valued for
predicates in S and all predicates on which they depend, so for every M satisfying FoundedClosed (π) ⊆
M , FoundedClosed (π) and M contain the same literals for those predicates, so SelfFalse π (M ) =
SelfFalse π (FoundedClosed (π)) and SelfFalse π′ (M ) = SelfFalse π′ (FoundedClosed (π)). For every instance R of a rule whose conclusion is for a predicate in S, every hypothesis of R is T or F
(not undefined) in FoundedClosed (M ), so disjunct (2) in the definition of self-false set cannot be
used to treat any additional hypothesis of R as F , regardless of which predicates are closed, so
SelfFalse π (FoundedClosed (π)) = SelfFalse π′ (FoundedClosed (π)). Using these equalities and transitivity, SelfFalse π (M ) = SelfFalse π′ (M ). Thus, the third condition is equivalent for the two programs.

Proof of Theorem 17. First, we show FoundedClosed (π) ⊆ WFS (π), by proving by induction
on the computation of the least fixed point that, in each step, Fπ (I) ⊆ WFS (π). The induction hypothesis is I ⊆ WFS (π), and we need to show Fπ (I) ⊆ WFS (π). It suffices to show (a)
Founded (π ∪ I) ⊆ WFS (π) and (b) ¬ · SelfFalse π (Founded (π ∪ I)) ⊆ WFS (π), since Fπ (I) is the
union of these two sets.
Proof of (a): By Theorem 10, Founded (π ∪ I) ⊆ WFS (π ∪ I). It is easy to show that, for any
subset I of WFS (π), WFS (π ∪ I) = WFS (π). Thus, Founded (π ∪ I) ⊆ WFS (π).
Proof of (b): SelfFalse π is monotone, and Founded (π ∪ I) ⊆ WFS (π) from (a), so
SelfFalse π (Founded (π ∪ I)) ⊆ SelfFalse π (WFS (π)). SelfFalse π is Uπ restricted to specified predicates, so SelfFalse π (I) ⊆ Uπ (I) for any interpretation I. Thus, SelfFalse(Founded (π ∪ I)) ⊆
Uπ (WFS (π)). By definition of WFS π , ¬·Uπ (WFS (π)) ⊆ WFS (π). Thus, ¬·SelfFalse (Founded (π ∪
I)) ⊆ WFS (π).
Second, we show WFS (π) ⊆ FoundedClosed (π), by proving by induction on the computation
of the least fixed point that, in each step, Wπ (I) ⊆ FoundedClosed (π). The induction hypothesis
is I ⊆ FoundedClosed (π), and we need to show Wπ (I) ⊆ FoundedClosed (π). It suffices to show
(a) Tπ (I) ⊆ FoundedClosed (π) and (b) ¬ · Uπ (I) ⊆ FoundedClosed (π), since Wπ (I) is the union
of these two sets. The proof of (a) is straightforward using the induction hypothesis and the
definitions of Tπ and Founded . Let Atom c and Atom u denote the set of all literals for predicates
declared certain and uncertain, respectively. We show (b) first for certain predicates and then
for uncertain predicates, i.e., we show (b1) ¬ · Uπ (I) ∩ Atom c ⊆ FoundedClosed (π) and then (b2)
¬ · Uπ (I) ∩ Atom u ⊆ FoundedClosed (π).
For (b1), consider a literal ¬A in ¬ · Uπ (I) ∩ Atom c . The definition of WFS (π) and monotonicity
of Wπ imply ¬A ∈ WFS (π). As shown above, FoundedClosed (π) ⊆ WFS (π), so FoundedClosed (π)
cannot contain A (if it did, WFS (π) would also contain A and would be inconsistent). The predicate
in A is certain, so FoundedClosed (π) is 2-valued for that predicate, and FoundedClosed (π) does not
contain A, so it must contain ¬A. Thus, ¬ · Uπ (I) ∩ Atom c ⊆ FoundedClosed (π).
25

The proof of (b2) uses the following lemma relating unfounded sets and self-false sets, which
is easily proved from the definitions: (Uπ (I) ∩ Atom u ) ⊆ SelfFalse π (I) when all uncertain predicates are complete and closed. For (b2), the induction hypothesis is I ⊆ FoundedClosed (π). Uπ is
monotone, so Uπ (I) ⊆ Uπ (FoundedClosed (π)). The above lemma implies Uπ (FoundedClosed (π)) ⊆
SelfFalse π (FoundedClosed (π)). By transitivity, Uπ (I) ⊆ SelfFalse π (FoundedClosed (π)). By definition of FoundedClosed , ¬ · SelfFalse π (FoundedClosed (π)) ⊆ FoundedClosed (π). Using this inequality, the preceding inequality, and transitivity, we conclude ¬ · Uπ (I) ⊆ FoundedClosed (π).

Proof of Theorem 18. Proof that SMS (π) ⊆ ConstraintClosed (π). Let M ∈ SMS (π). We
need to show M ∈ ConstraintClosed (π), i.e., (1) FoundedClosed (π) ⊆ M , (2) M is a model of
Cmpl (π), and (3) ¬ · SelfFalse π (M ) ⊆ M . The proof uses Theorem 14, which has the additional
hypothesis that all predicates have default declarations as certain or uncertain. Theorem 14 is
applicable here nevertheless, because that additional hypothesis is unnecessary in the context of the
other hypotheses of this theorem. To see this, note that non-default declarations of predicates as
certain or uncertain can differ from the default declarations only by unnecessarily declaring some
predicates uncertain. By hypothesis, those predicates must also be declared complete and closed. By
applying Theorem 16 to each SCC containing those predicates, we conclude that these non-default
declarations do not change the founded and constraint semantics.
Proof of (1): As shown in the proof of Theorem 14, WFS (π) ⊆ M . By Theorem 17,
FoundedClosed (π) = WFS (π), so FoundedClosed (π) ⊆ M . Proof of (2): Same as in the proof
of Theorem 14. Proof of (3): Every uncertain predicate is closed, so SelfFalse π (M ) ⊆ Uπ (M ), so
¬ · SelfFalse π (M ) ⊆ Wπ (M ). M is a fixed point of Wπ [VRS91, Theorem 5.4], so Wπ (M ) = M .
Using this to simplify the right side of the previous inequality, we conclude ¬ · SelfFalse π (M ) ⊆ M .
Proof that ConstraintClosed (π) ⊆ SMS (π). Let M ∈ ConstraintClosed (π). We need to show
M ∈ SMS (π); this is equivalent to showing M is a fixed point of Wπ [VRS91, Theorem 5.4]. We
prove Wπ (M ) ⊆ M and M ⊆ Wπ (M ).
Proof that Wπ (M ) ⊆ M : We need to show Tπ (M ) ⊆ M and ¬ · Uπ (M ) ⊆ M . The former
follows from the fact that M is a model of Cmpl (π).
The latter follows from ¬ · SelfFalse π (M ) ⊆ M and SelfFalse π (M ) = Uπ (M ), as shown next.
Since the definition of SelfFalse π (M ) is obtained from the definition of Uπ (M ) by limiting in the
recursive disjunct to closed predicates, SelfFalse π (M ) ⊆ Uπ (M ) always holds. Since all uncertain predicates are also closed, to show SelfFalse π (M ) = Uπ (M ), it suffices to show that, for
each atom A in Uπ (M ) for a certain predicate P , A ∈ SelfFalse π (M ). To see this, note that
¬A ∈ FoundedClosed π (M ), because FoundedClosed (M ) includes all negative literals for certain
predicates that can be in any consistent model of π (recall that certain predicates cannot depend on uncertain predicates, so this holds regardless of undefined values in FoundedClosed (M )).
Since ¬A ∈ FoundedClosed π (M ) and FoundedClosed π (M ) ⊆ M , we have ¬A ∈ M and hence
A ∈ SelfFalse π (M ).
Proof that M ⊆ Wπ (M ): Consider any literal in M . We need to show that the literal is in
Wπ (M ).
case 1: Consider a positive literal A in M . We show A ∈ Tπ (M ) hence A ∈ Wπ (M ).
case 1.1: A is for a certain predicate. FoundedClosed (M ) and M contain the same literals for such predicates, so A ∈ FoundedClosed (M ), so A ∈ Tπ (I), where I is the intermediate approximation to FoundedClosed (M ) at the step when A is added. Tπ is monotonic, and
I ⊆ FoundedClosed (M ) ⊆ M , so A ∈ Tπ (M ).
26

case 1.2: A is for a uncertain predicate P . M satisfies Cmpl (π). Cmpl (M ) contains the combined
rule C ← B for P and its inverse ¬C ← ¬B. M is 2-valued, and in 2-valued models, the conjunction
of these two rules is equivalent to C ⇔ B. Therefore, A is derivable in M using an instance of the
combined rule for P , which is logically equivalent to the original rules for P in π, so A ∈ Tπ (M ).
case 2: consider a negative literal ¬A in M . We show A ∈ Uπ (M ) hence ¬A ∈ Wπ (M ).
case 2.1: ¬A is for a certain predicate. FoundedClosed (M ) and M contain the same literals for
such predicates, so ¬A ∈ FoundedClosed (π). By Theorem 17, FoundedClosed (π) = WFS (π), so
¬A ∈ WFS (π), so A ∈ Uπ (FoundedClosed (π)), so by monotonicity, A ∈ Uπ (M ).
case 2.2: ¬A is for a uncertain predicate P . By reasoning similar to case 1.2, ¬A is derivable in
M using an instance of the inverse of the combined rule for P . By definition of the combined rule,
this implies that, for every instance with conclusion A of a rule for P in π, the body of the rule
evaluates to false in M . This implies A ∈ Uπ (M ).


27

