To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 27/04/01 - Paris - FR
Vous pouvez maintenant vous abonner à nos annonces de séminaires
http://pauillac.inria.fr/seminaires/subscribe.html
S E M I N A I R E
. ___
/ _ _ / _ /
/ / \ / \ / / __| /
|___ |_/ |_/ / |__ |_/ |_
___ . /
/ ___ __ /_ _ / _/ /| /| _ __ __ _ _
/ / / /_ / __| / / |/ | / \ /_ / / \ | / __|
|___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/
I N R I A - Rocquencourt
Salle de conference du Bat 11
Vendredi 27 avril, 10h30
------------------------------------------------
Martijn Oostdijk (joint work with Olga Caprotti)
------------------------------------------------
=====================================
How to prove Prime(1234567891) in Coq
=====================================
In this talk we present how proof assistants (PA) and computer algebra
systems (CAS) can be combined in order to get efficient yet formal
proofs.
We give a (skeptical) formalization of Pocklington's Criterion in the
PA Coq. This criterion states that to prove primality of a number, it
is sufficient to find a number of witnesses that satisfy certain
algebraic equalities. Finding those witnesses is a computationally
intensive task, best performed by a CAS. Therefore, we combine Coq to
a CAS using the OpenMath language.
The formalization of the criterion in Coq is interesting because we
are forced to prove a large amount of trivial and less trivial results
which are usually not explicitly mentioned in the informal proof.
The application to generate primality proofs demonstrates that
combining PAs and CASs is feasible and can be very helpful. It also
helps us understand the limitations of a PA with respect to
computations.
If time (and technology) permits, there will be a short system demo.