Automatic inductive theorem proving using Prolog (Q1103415)

The paper describes a theorem-proving method based on Prolog. The method is used for proving universally quantified propositions in first order theory. The proposition must be in the form of a Horn clause in which the consequence is an equality predicate. The authors give a detailed description of three new mechanisms: Skolemization by need, suspended evaluation, limited forward chaining. The power of the method is illustrated by proving inductive properties of Prolog programs. Functional and algorithmic descriptions of the prover are included. The present inductive theorem proving method is compared with the term rewriting method and the Boyer-Moore method. Finally, the authors shortly describe how the method can be used for program development and verification.