Constructive matching — A methodology for inductive theorem proving

Abstract

Constructive Matching (CM) is a methodology for proving by induction theorems which express formally specifications of programs, i.e., theorems of the form ∀ x ∃z Q(x,z). The principal feature of our methodology is its deterministic character.

We have applied this methodology to two basic problems in inductive theorem proving: (1) strategy for proving an atomic formula, and (2) strategy for solving a special kind of equations. In this paper we present our methodology and illustrate its explanatory character. In particular, we try to show that our method provides explanations, as much as possible, in terms of the original problem, which makes them understandable for the user and suitable for the system.

The paper uses the vocabulary presented in [10].