Evènement pour le groupe Séminaire Méthodes Formelles


Date 2018-03-06  11:00-12:00
TitreThe hydra and the rooster 
RésuméThe Hydra game was introduced in 1982 by the mathematicians L. Kirby and J. Paris in their article: "Accessible Independence Results for Peano Arithmetic". This article contains two theorems: 1. Whichever the strategy of Hercules and the Hydra, any battle eventually terminates with Hercules' victory. 2. The previous result cannot be proved in Peano Arithmetic. We present a formal, self-contained (axiom-free) proof of a variant of both theorems, with the help of the Coq proof assistant. Since Coq's logic is higher-order intuitionnistic logic, the reference to Peano Arithmetic is replaced with a study of a class of proofs of termination indexed by ordinal numbers less or equal than epsilon_0. We present the main parts of this proof, as well as the main features of Coq that made its construction possible. 
Lieu178 
OrateurPierre Casteran 
Emailhttp://www.labri.fr/perso/casteran/ 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index