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.independent

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 ]
MeAmI.org

Posts: 405
Registered: 6/14/09
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 22, 2009 4:19 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply



William Elliot wrote:
> On Sun, 21 Jun 2009, Andrew Tomazos wrote:
>

> > Please consider the following formal proof language example:
> >

> It's a pain in the butt to read.
> Here's the same which is much easier to read.
>
> Let N be the natural numbers.
> Proposition. For all a,b,c in N
> if a is odd, a,b are relative prime and
> a^2 + b^2 = c^2,
> then there's some m,n in N for which m <= n,
> a = n^2 - m^2,
> b = 2mn,
> c = n^2 + m^2.
> Proof. ...
>

> > package MyTheoryProof;
> > using edu.mit.number_theory.*;
> >
> > theorem MyTheory
> > {
> > let N be NaturalNumbers;
> > forall a, b, c in N
> > given
> > {
> > a^2 + b^2 = c^2;
> > a, b are_relative_prime;
> > a is odd;
> > }
> > implies
> > {
> > m <= n;
> > a = n^2 - m^2;
> > b = 2 * m * n;
> > c = n^2 + m^2;
> > }
> > }
> > proven_by
> > {
> > ...
> > }
> >
> > This is written in a Mizar-like language with some formatting changes
> > based on the C family tree and some personal touches.
> >
> > Without any description of the language, I'm curious to know whether
> > you can derive the meaning of the theorem statement simply by reading
> > the code? The goal is for it to be both machine and human readable.
> >
> > Thanks,
> > Andrew.
> >
> > --
> > Andrew Tomazos <andrew@tomazos.com> <http://www.tomazos.com>
> >


Thank you
Referencing my work:(http://www.groupsrv.com/science/
about423882.html /)


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.