Sciweavers

Share
SLP
1993

Logic Program Specialisation With Deletion of Useless Clauses

8 years 9 months ago
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...
D. Andre de Waal, John P. Gallagher
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1993
Where SLP
Authors D. Andre de Waal, John P. Gallagher
Comments (0)
books