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.
Type de document :
Autre publication
Version finale envoyé a Springer. 2011
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00692193
Contributeur : Helene Kirchner <>
Soumis le : dimanche 29 avril 2012 - 10:19:58
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 03:28:02

Fichier

hg2011.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00692193, version 1

Collections

Citation

Claude Kirchner, Helene Kirchner, Fabrice Nahon. Narrowing Based Inductive Proof Search. Version finale envoyé a Springer. 2011. 〈hal-00692193〉

Partager

Métriques

Consultations de la notice

224

Téléchargements de fichiers

90