CHOOSING AN INDUCTION VARIABLE IN UNIVERSALLY QUANTIFIED ATOMIC FORMULAS

Autre Publication Année : 2015

(1) , (2)

1
2

Marta Franova

Machine Learning and Optimisation

Yves Kodratoff

Laboratoire de Recherche en Informatique

The paper presents an algorithm for choosing an induction variable for "lazy' induction proofs.

Constructive Matching Methodology inductive theorem proving induction variable

Intelligence artificielle [cs.AI]

Fichier principal

RR1579.pdf (147.76 Ko)

Origine : Fichiers produits par l'(les) auteur(s)

https://inria.hal.science/hal-01131271

Soumis le : jeudi 26 mars 2015-10:11:34

Dernière modification le : jeudi 29 février 2024-03:30:50

Archivage à long terme le : lundi 17 avril 2017-11:42:56

hal-01131271 , version 1 (26-03-2015)

Marta Franova, Yves Kodratoff. CHOOSING AN INDUCTION VARIABLE IN UNIVERSALLY QUANTIFIED ATOMIC FORMULAS. 2015, pp.15. ⟨hal-01131271⟩

CNRS INRIA UMR8623 CENTRALESUPELEC INRIA2 LRI-AO UNIV-PARIS-SACLAY GS-COMPUTER-SCIENCE

76 Consultations

131 Téléchargements