Re: [GeOCaml] Demonstration vs aide à la pr euve...

[Julien Narboux]

Arnaud Doniec a écrit :

> rebonjour à tous,
>
> Je me lancer à l'eau avec une première question pour Julien...
> Quand tu parles de démonstration automatique, tu parles d'une moulinette
> qui prend en entrée un problème donné et te ressort une
> démonstration 'toute faite' ? ou alors d'une aide (interactive) à la
> preuve ?
>  

La première solution, j'ai implémenté en Ltac (le langage de tactique de 
Coq) une tactique qui permet pour l'instant en gros de traiter la 
géométrie de l'incidence (mais c'est en cours d'extension). J'utilise la 
méthode de Chou,Gao, Zhang qui consiste à éliminer les points construits 
du but (le théorème que l'on est en train de prouver) au moyen de lemmes 
préalablement prouvés. Quand tous les points construits sont éliminés  
il reste que les points libres, et on sait s'en débrouiller.

Pour de plus amples informations et des références au bouquin de 
Chou,Gao, Zhang voir : 
http://www.lix.polytechnique.fr/Labo/Julien.Narboux/papers/GeometryInCoqTphol04.ps.gz