Proof reconstruction (preliminary version).
Judicaël Courant, Centre National de la Recherche Scientifique (CNRS), 69 - Lyon (France). Lab. de l'Informatique du Parallelisme, Ecole Normale Superieure de Lyon, 69 (France). Lab. de l'Informatique du Parallelisme, Lyon-1 Univ., 69 (France). Lab. de l'Informatique du Parallelisme · OpenGrey (Institut de l'Information Scientifique et Technique) · 1996
In the field of formal methods, rewriting techniques and provers by consistency in particular appear as powerful tools for automating deduction. However, these provers suffer limitations as they only give a (non-readable) trace of their progress and a yes/no answer where the user would expect a detailed explicit proof. Therefore, we propose a general mechanism to build an explicit proof from the running of a generic class of inductionless induction provers. We then show how it applies to Bouhoula's SPIKE prover, and give examples of proofs built by this method.