Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal Proof Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 Jan Burse Posts: 1,472 Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 5:04 PM

Jan Burse schrieb:
> Except maybe the "," in Prolog, which has the meaning of a kind of
> a conjunction. But in Prolog the "," is mostly treated as any other
> operator. With a level and a associativity etc.. So maybe we can
> advance the discussion as follows. You want the following operator:
>
> ";" : Conjunction
> "forall" : Universal quantifier
> "implies": Implication
> "thereexists" : Existential quantifier
>
> Ok, now tell me, how will the story continue for proof figures?

(c) Jan Burse

Ok, here is a hint. Proofs are usually a mesh.
So it is quite crucial that axioms, lemmas, etc..
can be labled. At least this is one approach,
and it can practically not be avoided.

In normal programming languages we have a many
objects that are nameable. For example variables
and functions. This is alreay quite nice, since
they are on different levels. And a similar thing
will also happen to proofs.

So there will be proofs where the mathematician
himself will give names, in the form of lemmas,
subtheorems, etc.. We could use function object syntax
for that:

lemma helper1 {
}

lemma helper2 {
}

And there will be proof steps, the mathematician
is refering in his phrasing of the proofs. We could
use variable object syntax for that:

step line21 =
lamma helper2 {
step line22 =

}

We can only introduce local variables, when the step
is really not used outside. So we will have local and
global steps. And the step itselfs will be not tactics,
but inference rule applications, or axiom schema
instantiations. Something like:

step line21 = eqReflex("y");
lemma helper2 {
step line22 = modusPonens(line21,helper1);
return line22;
}

The verification could also be done by constant evaluation,
a compiler could do this at compile time. We could combine
proofs and other code. Maybe use proofs in assertions. Wow!

Does this make sense to you?

Bye

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir