The Applicability of Logic Program Analysis and Transformation to Theorem Proving

Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can be used to infer useful information that can speed up theorem provers, assist in the identification of necessary inference rules for solving specific problems, how failure branches can be eliminated from the proof tree and how a non-terminating deduction in a proof system can be turned into failure. In addition, this method also provides sufficient conditions for identifying Case-free Theories [26]. The specialisation techniques developed in this paper are independent of the proof system and can therefore be applied to theorem provers for any logic written as logic programs. 1 Introduction Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can be used to infer nontrivial result..