Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Jan Burse

Posts: 463
Registered: 4/12/05
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 5:04 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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
Read Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/26/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Jan Burse
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Joshua Cranmer
6/27/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Marshall
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Spiros Bousbouras
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Tim Smith
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
Charlie-Boo
6/21/09
Read Re: Formal Proof Language Example - Human-Readable?
William Elliot
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/22/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/23/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
David Bernier
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
MeAmI.org
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/24/09
Read Re: Formal Proof Language Example - Human-Readable?
Andrew Tomazos
6/25/09
Read Re: Formal Proof Language Example - Human-Readable?
Slawomir

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.