Definitions

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.

An interpretation I for a logic program S with classical negation is defined in the 'classical' manner. That is, I is an assignment of truth value TRUE and FALSE to each term in S such that it assigns the same truth value to the 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 S |=p.

Clause trees and supported propositions

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₂, ..., _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.

If there is a closed clause tree rooted at p, then p is said to be evident. If both p and its negation ~p are evident then p is said to be conflicted.

Proposition p is supported provided that there is a closed clause tree T rooted at p such that none of the interior nodes in T is conflicted. By definition, if p is supported, then it is evident.

An example

Consider the following logic program:

a <- b, ~c, d.        ~a <-      
b <-                  ~b <- e, f.    ~c <- ~b.      ~c <-         
d <- ~a.              d <-  e.          
e <-  c.              e <-  a, f.    f <-



Four sample clause trees are shown here. Note that only T1 and T2 are closed.. Only a, ~a, b, ~b, ~c, d, e, and f are evident. a, ~a, b, and ~b are conflicted. Only ~a, b, ~c, and f are supported.

Whether the above definition of 'evident' and 'support' are 'intuitive' is debatable. We simply argue that it is useful to define and talk about 'evident' and 'support' in the manner described here without claiming, for instance, that this is in fact what people really mean when they use these terms.

Returning to tree T1 in the example, note that the subtree rooted at c is itself a closed clause tree. In contrast, the subtree rooted at b is not a closed clause tree. Hence, there is a difference between c and b which can be made explicit through the notion of a contingency annotated closed clause tree.

A contingency annotated closed clause tree T rooted at p is a closed clause tree rooted at p where each node in T is annotated with a set of contingencies as follows:

• each 'true' leaf is annotated with the empty set {}.
• each non-true leaf is annotated with a set containing solely of its negation.
• each non-leaf node is annotated with the union of its children's contingency sets minus itself; i.e., if node n has children nodes n₁, n₂, ..., n_k whose contingency sets are C₁, C₂, ..., C_k respectively, then n is annotated with the set C₁, C₂, ... C_k \ {n}.

Here is T1 with contingency set annotation

In a contingency annotated closed clause tree, any node with a non-empty contingency set is called a contingent node. An interior node with an empty contingency set is called a supporting node. In T5, b is a contingent node while c is a supporting node. Roughly speaking, a contingent node is a node that was involved in case-based reasoning. It is not necessary to commit to any truth value concerning a contingent node [Fisher95]. In T5, for example, b is neither evident nor supported but is used 'in a contingent manner' to support c. A supporting node, on the other hand, is a stronger assertion since it is itself evident and possibly supported.