Proof reconstruction (preliminary version).

Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101787
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:06:14 AM
Last modification on : Wednesday, November 20, 2019 - 2:54:29 AM

File

RR1996-26.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101787, version 1

Collections

Citation

Judicael Courant. Proof reconstruction (preliminary version).. [Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p. ⟨hal-02101787⟩

Share

Metrics

Record views

17

Files downloads

7