TY - GEN
T1 - Proof Plans for the Correction of False Conjectures
AU - Monroy,Raul
AU - Bundy,Alan
AU - Ireland,Andrew
PY - 1994
Y1 - 1994
N2 - Theorem proving is the systematic derivation of a mathcmaticM
proof from a set of axioms by the use of rules of inference. We ~re
interested in a related but far less explored problem: the analysis and
correction of false conjectures, especiMly where that correction involves
finding a collection of antecedents that, together with a set of axioms,
transform non-theorems into theorems. Most failed search trees are huge,
and special care is to be taken in order to tackle the combinatorial explosion
phenoraenom Fortunately, the planning search space generated
by proof plans, see [1], are moderately small. We have explored the possibility
of using this technique in the implementation of an abduction
mechanism to correct non-theorems.
AB - Theorem proving is the systematic derivation of a mathcmaticM
proof from a set of axioms by the use of rules of inference. We ~re
interested in a related but far less explored problem: the analysis and
correction of false conjectures, especiMly where that correction involves
finding a collection of antecedents that, together with a set of axioms,
transform non-theorems into theorems. Most failed search trees are huge,
and special care is to be taken in order to tackle the combinatorial explosion
phenoraenom Fortunately, the planning search space generated
by proof plans, see [1], are moderately small. We have explored the possibility
of using this technique in the implementation of an abduction
mechanism to correct non-theorems.
M3 - Conference contribution
BT - Proceedings of Logic Programming and Automated Reasoning '94
ER -