Skip to Main content Skip to Navigation
Other publications

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 metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Helene Kirchner Connect in order to contact the contributor
Submitted on : Sunday, April 29, 2012 - 10:19:58 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Thursday, December 15, 2016 - 3:28:02 AM


Files produced by the author(s)


  • HAL Id : hal-00692193, version 1



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



Record views


Files downloads