Answer Extraction
- Resolution can be used to answer the questions but it is complex than proving a theorem.
- This method is invented by green 1969b and has been extended by Luckham and Nilsson.
- If we want to prove a theorem of the form (∃r) ω(r) or want to produce r which we have proven exist we must use a device of an answer literal to keep track of substitutions made during the refutation process.
- That is, the literal Ans (r1, r2,...) is added to every clause which comes from the negation of the theorem to be proved and the refutation is performed until the answer literal is left.
- In the answer literal, the variables are those which are found in the negation of the theorem which is to be proved.
- In the answer literal, the terms substituted for variables during proof are the instances of variables which are existentially quantified in the well formed formula that has to be proved.
- Example: We can see the use of answer 1 literal in Figure.
- Let us now prove the wff. (∃u) I (B, u) where the robot asks "In which room is" for itself.
Fig: Answer Extraction
- It can be seen from the above Figure that the answer literal is added. to the negation of the theorem to be proved and continued until only the answer literal is left.
