Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01216750
Contributor : Julien Narboux <>
Submitted on : Friday, October 16, 2015 - 7:58:40 PM
Last modification on : Saturday, October 27, 2018 - 1:23:54 AM
Long-term archiving on: : Thursday, April 27, 2017 - 7:15:13 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01216750, version 1

Citation

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

Share

Metrics

Record views

411

Files downloads

207