Predicate Synthesis and other Fault Correction 
Techniques via Recursion-Editor and Abduction Techniques




and program synthesis


The use of automated reasoning in 
theorem proving task such as program synthesis, 
the speculation of a bridging lemma or 
the generalisation of an input conjecture often 
ends up with an unprovable, faulty conjecture. 
A successful subsequent construction attempt highly depends 
on a quick correction of the conjecture 
fault. Hence, it is highly desirable to 
have an automated means for explaining why 
a conjecture is faulty and how it 
can be corrected. We introduce a fully 
automatic abduction-based mechanism for the correction of 
faulty conjectures. The mechanism works on top 
of an automatic theorem prover. If the 
prover is given a faulty conjecture, $\forall 
X.\,G(X)$, the mechanism will identify a corrective 
predicate, $P(X)$, such that $\forall X.\,P(X)\rightarrow G(X)$ 
is a theorem. A definition for $P(X)$ 
is provided. The synthesis of $P(X)$ is 
a program transformation task. The mechanism consists 
of a collection of construction commands. A 
construction command is a small program, expressed 
in a meta-language, containing one or more 
recursive, program editing commands. The application of 
a construction command performs a transformation in 
the definition of a corrective predicate. Each 
construction command is associated with an inference 
rule. If a rule is applied, so 
is its corresponding construction command. The association 
of a construction command is commanded by 
the constructive principle of formulae as types: 
if an induction rule is applied, the 
construction command is such that it attempts 
to make the corrective predicate recursive. The 
mechanism yields a corrective predicate that is 
guaranteed to be well-defined. If recursive, the 
predicate will also be terminating.