From: Torkel Franzen <torkel@sm.luth.se>
Subject: Re: structured theorem proving; state of the art in proof-checking programs
Date: 03 Feb 2000 12:56:30 +0100
Newsgroups: sci.math,sci.logic
Summary: [missing]

David Bernier <bernier@my-deja.com> writes:

  > This is just a draft;  any comments are welcome.

  Such projects exist, in particular the Mizar project. See
http://mizar.org/.
==============================================================================

From: Adriaan de Groot <adridg@aramis.cs.kun.nl>
Subject: Re: structured theorem proving; state of the art in proof-checking programs
Date: 3 Feb 2000 14:07:40 GMT
Newsgroups: sci.math,sci.logic

In sci.math David Bernier <bernier@my-deja.com> wrote:
> It strikes me how "easy" it is to write down a correct proof in
> the non-formal "mathematical vernacular" (given e.g. a detailed
> sketch) while it's not so easy to write a bug-free program for
> a medium-difficulty task (given a precisely formulated algorithm);
Yup, but trying to (re-)do a proof  in natural deduction style often
shows up a number of problems in your original so-called proof. This
is just a question of minor sloppiness in the "mathematical vernacular".

> I am quite interested, for this reason, in formal proof-checkers
> for which the following would be desirable features (BTW, I
> know very little about what has already been done in  this area.)
Well, fire up your web browser and look at:

1) PVS, which has pretty much all the features you describe and
   a *vast* amount of (mostly comp.sci) case studies. (www.csl.sri.com)
2) Coq, which is based on type theory and is very rigorous and
   very tedious to use. (www.inria.fr)
3) Isabelle/HOL (www.in.tum.de/~nipkow)

Me, I work mostly with PVS. I've tried to do some stuff on monoids in
PVS and I believe it will work if you put in enough time. The problem being
first getting all the group and ring theory in PVS - I don't know of any 
libraries for PVS doing that kind of straightforward algebra.


> (a) the formal language for the proof checker ("PF") should
>     be user-friendly.

How's this?


foozle : THEORY
BEGIN
V : TYPE+ ;
< : (linord?);
inconsistency : ( EXISTS (v:V) : v<v ) => (0=1) ;
END foozle

ie. assume some non-empty set V and a strict linear ordering on V,
then the assumption that < is reflexive leads to inconsistency.
Not that this is interesting news, but it's just a real short
overview of PVS' syntax. Note that PVS does a certain amount of
"helping" along the way - it's not *just* a verifier. Coq is more
of a pure verifier.

> (c) PF should have the capacity to handle user-defined structures,
>     e.g. functions, predicates, proven theorems with user-chosen
>     names and so on.
Both Isabelle/HOL and PVS have a rich polymorphic yadda yadda type system.