Meta-interpreter to Build Proof Trees

(15th-July-2020)

• To implement the how command of Section 5.3.3.1, the interpreter maintains a representation of the proof tree for a derived answer. Our meta-interpreter can be extended to build a proof tree. Figure 13.13 gives a meta-interpreter that implements built-in predicates and builds a representation of a proof tree. This proof tree can be traversed to implement how questions.

Ask the User Meta-interpreter

• % aprove(G) is true if base-level body G is a logical consequence of the base-level knowledge base and the answers provided by asking the user yes/no questions.