Reasoning in default logic

• The possible nonexistence of extensions is a problem, then there are 2 alternative solutions :

  1. Resitrct attention to those classes of default theories for which the existence of extensions is guaranteed (normal default theories)
  2. Modify the concept of an extension in such a way that all default theories have at least one extension (not in this course)
• A default is called normal if its consequent is its only justification P:Q / Q

  in normal default theories all defaults are normal
• Normal default theories :

  • always have extensions
  • rule out pathological cases such as $T : \frac{p}{\neg p}$
  • have the limited expressive power
• T = (W,D) : a normal default theory :

  assume that W is satisfiable. Then :

  • each process of T is successful
  • T always possesses extensions. Every finite process Pi of T may be explaneded to a closed process
• Normal default theories are semi-monotonic : the addition of default rules never eliminates but extends or adds new extensions
• theorem proving : knowing whether a specific formula is included in an extension of a default theory T, it is not appropriate to start determining extensions of T blindy
• normal theoreis admit a goal-oriented reasoning method : backward-chaining, based on linear resolution

  
  

  we consider here a special case : closed normal default theoreis and closed formulas
• Example

  A) normal

  B) non-closed

  C) normal

  D) closed

  
• Lineair resolution (idea)

  • start with a clause
  • resolve it against a clause to obtain a resolvent
  • resolve this resolvent against some clause
  • and so on, until the empty clause is obtained
• A default proof of F in a closed normal default theory T = (W,D) is a finite sequence (D_0, .. D_k) of subsets of D such that :

  1. F follows from W union Cons(D_0)
  2. forall 1 =< i =< K , the prerequistes of defaults in D_(i-1) follow from W union cons(D_i)
  3. D_k = empty
  4. W union U cons(D_i) is satisfiable
• Theorem Soundness and completeness : let F be a closed formula. A consistent closed normal default theroy T has an extension containg F iff there is a default proof of F in T.
• We define the set of clauses of T as : Clauses (T) = $\{ (C, \{ d \}) | d \in D$ and (C, {d}) is a consequent of caluse of $\{ d \cup \{(C, \empty \} | C \in W \}$
• A pair (C, D') where C is aclause and D' in D is a set of normal defaults, will be referred to as an indexed clause.
• A resolvent of (C_1, D_1) and (C_2, D2)

  if R is a usual resolvent of C1 and C2 then the index clause R,D1 union D2
• The top-down proof method can be generalized from closed normal defaults to open normal defaults
• A top-down default proof of a closed formula F with respect to a closed normal default hteory is a seuqne of linear resolutions proofs such that :

  1. L_0 is a linear resolution proof of F from clauses(T)
  2. for 0 =< i =< k , L_i returns D_i
  3. for I =< i =< k, L_i is a linear reoslution proof of pre(D_i-1) from clauses T
  4. D_k = empty
  5. W uninon U Pcons(D_I)} is satisfiable