Narrowing Based Inductive Proof Search

Claude Kirchner 1 Helene Kirchner 1 Fabrice Nahon 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present in this paper a narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to yield a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be sound and refutationally correct in a proof theoretical way.
Document type :
Other publications
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-00692193
Contributor : Helene Kirchner <>
Submitted on : Sunday, April 29, 2012 - 10:19:58 AM
Last modification on : Thursday, January 11, 2018 - 6:22:10 AM
Long-term archiving on : Thursday, December 15, 2016 - 3:28:02 AM

File

hg2011.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00692193, version 1

Collections

Citation

Claude Kirchner, Helene Kirchner, Fabrice Nahon. Narrowing Based Inductive Proof Search. 2011. ⟨hal-00692193⟩

Share

Metrics

Record views

254

Files downloads

175