Automatic inductive theorem proving using Prolog

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 (Stickel, 1984). In this paper, we introduce a Prolog-based deductive theorem proving method for proving theorems in a 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 of the subdomains 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 mechanism—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 describe how the theorem prover can be used to prove properties of Prolog programs by showing two simple examples.

rivista o collana

 Theoretical Computer Science (TCS)