Background

Preliminary

Logic programs

A logic program S with classical negation is a finite collection of directed clauses, each of which has the form :
p <- q₁, q₂, ..., q_n.

where n >= 0, <- is the implication operator, commas represent conjunction, and p, q₁...q_n are either positive or negative terms. Each directed clause also has an equivalent disjunctive form:

p v ~q₁ v ~q v ~q₂ v ... v ~q_n.

The classical negation of term p is ~p; double negations are absorbed. For example, the negation of ~s(a) is s(a) and vice versa. p <- is equivalent to p <- true.

An interpretation for a logic program S with classical negation is defined the usual way, that is, as an assignment I of truth value TRUE or FALSE to terms and clauses in S as follows:

• for the atoms 'true' and 'false':
  • I(true) := TRUE
  • I(false) := v FALSE

• for any term p:
  • I(p) := TRUE iff I(~p) = FALSE
  • I(p) := FALSE iff I(~p) = TRUE

• for any clause in S:
  • I(p <- q₁, q₂, ..., q_n) := FALSE iff
    I(q_i) = TRUE for 1 <= i <= n, AND
    I(p) = FALSE.
  • I(p <- q₁, q₂, ..., q_n) := TRUE otherwise.

Note that any such interpretation assigns the same truth value to each directed clause as a 'classical' interpretation does to the corresponding disjunctive clause. An assignment I that assigns TRUE to every clause in logic program S is called a model for S. If there exists a model for S, then S is said to be consistent or satisfiable; otherwise, S is inconsistent or unsatisfiable. If every model for S also assigns TRUE to some proposition p, then p is a logical consequence of S, written as S |= p.

Clause trees

Let S be a logic program with classical negations and let p be a term in S. A clause tree T rooted at p is either:
• p itself, or
• a tree rooted at p and having unordered children T₁, T₂,..., T_k, where T₁, T₂, ..., T_k are clause trees rooted at q₁, q₂, ..., q_k respectively, and p <- q₁, q₂, ..., q_k is a clause appearing in S.

A closed clause tree T rooted at p is a clause tree rooted at p such that every leaf q in T is either:

• 'true', or
• a descendent of some node q' in T such that q' is the classical negation of q.