A reflexive tactic for automated generation of proofs of incidence to an affine variety

Pierre Boutry 1 Julien Narboux 1 Pascal Schreck 1
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Abstract : This paper describes the formalization and implementation of a reflexive tactic for automated generation of proofs of incidence to an affine variety. Incidence proofs occur frequently in formal proofs of geometric statements. Nevertheless they are most of the time omitted in pen-and-paper proofs since they do not contribute to the understanding of the proof in which they appear. Our tactic allows us to automate proofs about incidence to an affine variety. Being based on a type class capturing the minimal set of properties needed to deal with incidence, the tactic is applicable to any theory verifying these properties. This type class is defined using dependent types to formalize predicates of parameterizable arity which represent the incidence to an affine variety.
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01216750
Contributeur : Julien Narboux <>
Soumis le : vendredi 16 octobre 2015 - 19:58:40
Dernière modification le : jeudi 29 mars 2018 - 09:10:05
Document(s) archivé(s) le : jeudi 27 avril 2017 - 07:15:13

Fichier

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

Identifiants

  • HAL Id : hal-01216750, version 1

Collections

Citation

Pierre Boutry, Julien Narboux, Pascal Schreck. A reflexive tactic for automated generation of proofs of incidence to an affine variety. 2015. 〈hal-01216750〉

Partager

Métriques

Consultations de la notice

214

Téléchargements de fichiers

140