The need for Ancestor Resolution when answering queries in Horn clause logic

Prolog Technology Theorem Proving. (PTTP) [5] is a well known extension of Prolog for answering queries in first-order logic. PTTP is based on the idea that ‘Prolog can be viewed as an “almost complete ” theorem prover, which has to be extended by only a few ingredients in order to handle the non-Horn case ’ [1]. As explained in [5], PTTP is an efficient realisation of the Model Elimination (ME) calculus [2] that utilises five extensions of standard Prolog: 1. It uses a sound unification algorithm with the occur-check; 2. It uses a complete search strategy based on iterative-deepening; 3. It adds contrapositives of the clauses in the theory in order to provide entry points for all of the literals in those clauses; 4. It uses ancestor resolution when unfolding the query in order to overcome the incompleteness of Prolog’s SLD resolution; 5. It adds contrapositives for the negation of the query in order to extract indefinite answers from successful computations. Although it is equipped for full clausal reasoning, PTTP has been tailore