Proof Procedures for Complete Knowledge

(17th-August-2020)

• There are two types procedure.

1. Bottom-Up Procedure

2. Top-Down Negation-as-Failure Procedure

• The bottom-up procedure for negation as failure is a modification of the bottom-up procedure for definite clauses. The difference is that it can add literals of the form ∼p to the set C of consequences that have been derived; ∼p is added to C when it can determine that p must fail.

• Failure can be defined recursively: p fails when every body of a clause with p as the head fails. A body fails if one of the literals in the body fails. An atom bi in a body fails if ∼bi has been derived. A negation ∼bi in a body fails if bi has been derived.