Predicate synthesis for correcting faulty conjectures: The proof planning paradigm uri icon

Abstract

  • The synthesis of programs as well as other synthetic tasks often end up with an unprovable, partially false conjecture. A successful subsequent synthesis attempt depends on determining why the conjecture is faulty and how it can be corrected. Hence, it is highly desirable to have an automated means for detecting and correcting faulty conjectures. We introduce a method for patching faulty conjectures. The method is based on abduction and performs its task during an attempt to prove a given conjecture. On input ¿X. G(X), the method builds a definition for a corrective predicate, P(X), such that ¿X. P(X) ¿ G(X) is a theorem. The synthesis of a corrective predicate is guided by the constructive principle of formulae as types, relating inference with computation. We take the construction of a corrective predicate as a program transformation task. The method consists of a collection of construction commands. A construction command is a small program that makes use of one or more program editing commands, geared towards building recursive, equational procedures. A synthesised corrective predicate is guaranteed to be correct, turning a faulty conjecture into a theorem. Whether conditional or not, it will be well-defined. If recursive, it will also be terminating. Our method is amenable to mechanisation, but careful search guidance is required for making a productive use of the failure of a proof. A failed proof attempt quickly yields a huge, possibly infinite, deduction tree, giving rise to exponentially many abductive explanations. We suggest that a proof planning approach can structure the task of correcting a formula in such a way as to allow significant automation, while dramatically restricting the search space.

Publication date

  • July 1, 2003