CHOOSING AN INDUCTION VARIABLE IN UNIVERSALLY QUANTIFIED ATOMIC FORMULAS

Marta Franova 1 Yves Kodratoff 2
1 Apprentissage et Optimisation
LRI - Laboratoire de Recherche en Informatique
2 LRI - Laboratoire de Recherche en Informatique
Abstract : The paper presents an algorithm for choosing an induction variable for "lazy' induction proofs.
Keywords : induction variable inductive theorem proving Constructive Matching Methodology
Type de document :
Autre publication
Rapport de Recherche. 2015, pp.15
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01131271
Contributeur : Marta Franova <>
Soumis le : jeudi 26 mars 2015 - 10:11:34
Dernière modification le : mardi 24 avril 2018 - 13:38:55
Document(s) archivé(s) le : lundi 17 avril 2017 - 11:42:56

Fichier

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

Identifiants

  • HAL Id : hal-01131271, version 1

Collections

UMR8623 | UNIV-PARIS-SACLAY | INRIA | CENTRALESUPELEC

Citation

Marta Franova, Yves Kodratoff. CHOOSING AN INDUCTION VARIABLE IN UNIVERSALLY QUANTIFIED ATOMIC FORMULAS. Rapport de Recherche. 2015, pp.15. 〈hal-01131271〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

115

Téléchargements de fichiers

56

Contact


archive-ouverte@inria.fr