PROLOG-based inductive theorem proving

Abstract

Although PROLOG is a programming language based on techniques from theorem proving its use as a base for a theorem prover has not been explored until recently ([Sti84]). In this paper, we introduce a PROLOG-based deductive theorem proving method for proving first order inductive theory representable in Horn clauses. The method has the following characteristics: (1) It automatically partitions the domains over which the variables range into subdomains according to the manner in which the predicate symbols in the theorem are defined. (2) For each subdomain of the domain the prover returns a lemma. If the lemma is true, then the target theorem is true for this subdomain. The lemma could also be an induction hypothesis for the theorem. (3) The method does not explicitly use any inductive inference rule. The induction hypothesis, if needed for a certain subdomain, will sometimes be generated from a (limited) forward chaining mechanism in the prover and not from employing any particular inference rule.

In addition to the backward chaining and backtracking facilities of PROLOG, our method introduces three new mechanisms — skolemization by need, suspended evaluation, and limited forward chaining. These new mechanisms are simple enough to be easily implemented or even incorporated into PROLOG. We demonstrate the use of the theorem prover for verifying PROLOG programs and proving properties of data types.