Bonjour à tous,
Le dernier séminaire avant la pause estivale aura lieu ce jeudi 7 juillet.
Assia Mahboubi viendra nous présenter un travail qu'elle a effectué avec Cyril Cohen:
Assia Mahboubi (LIX)
Jeudi 7 juillet à 11h en salle 0C2
Résumé:
The decidability of the first order theories of (discrete) algebraically closed fields and (discrete) real closed fields are well-known results after Tarski's pioneering work in the 40's. Formalizing these proofs in a proof assistant like the Coq system legitimates classical reasoning inside models of these logical fragments, and can also provide complete proof-producing decision procedures for non-linear arithmetic. In this talk we explain how to develop modular formal proofs of quantifier elimination by separating the operations on formulas from the projection theorem at the core of these kind of proofs. The algorithm producing the quantifier free formula is programmed in continuation passing style, which leads to both a concise program and an elegant proof of semantic correctness.
(Joint work with Cyril Cohen)
=======
À NOTER: il y aura café, thé, etc... un quart d'heure avant le début du séminaire: venez un peu en avance!
=======
Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.
Amicalement,
Alexis
Aucun commentaire:
Enregistrer un commentaire