Logic Program Specialisation With Deletion of Useless Clauses

In this paper we describe a method of programspecialisation and give an extended example of its application to specialisation of a refutation proof procedure for rst order logic. In the specialisation method, a partial evaluation of the proof procedure with respect to a given s rst obtained. Secondly an abstract interpretation of the partially evaluated program is computed, and this is used to detect and remove clauses that yield no solutions useless clauses. A proof is given that such clauses can be deleted from a normal program while preserving the results of all nite computations. The model elimination proof procedure described in 20 is specialised with respect to given theories, and the negative ancestor check inference rule can be eliminated in cases where it is not relevant. Our results for the model elimination prover, obtained by general-purpose transformations, are comparable to those obtained in 20 by a special-purpose analysis. It is shown that specialisations of the proo...

• Type: Conference
• Year: 1993
• Where: SLP
• Authors: D. Andre de Waal, John P. Gallagher
• Keywords: Partial Evaluation, Proof Procedure, Refutation Proof Procedure, SLP 1993