Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
The hydra and the rooster
du 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