Towards Intelligent Inductive Proof Engineering

Abstract

This paper deals with inductive theorem proving (ITP for short). It does not provide new theoretical results but analyses existing ITP methods from an AI point of view. The presentation is based on the implicit ITP approach, i.e. ITP using the well-developed framework of rewriting and completion techniques for systems of equations and rewrite rules. We think that the relevant practical problems for successful (partially) automated ITP are essentially the same as or at least closely related to those occurring in the more conventional framework of explicit ITP using schemas. The theoretical foundations of implicit ITP are briefly reviewed focussing on the central ideas as well as on important operationalization issues. Moreover, a brief comparison of explicit and implicit ITP approaches is included. In particular, we clarify some criticisms raised against the implicit ITP approach. The main part of the paper is devoted to a thorough discussion of central ITP problems from the viewpoint of system designers and users. We point out and exemplify the necessity of linking together the whole process of formalizing, modelling and structuring abstract (equational) specifications of algorithms and corresponding (inductive) properties to be verified. Crucial aspects of the whole specification and proof engineering process are isolated and discussed, in particular conceptual and proof-technical ones. We argue that such an analysis (which of course has to be continued and deepened) is necessary for an adequate integration and combination of intelligent user-guided and machine-supported automated inductive reasoning. Finally the main theoretical and practical problems as well as promising perspectives for future work are sketched, in particular concerning architectural and design principles for future generation inductive theorem provers.