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 ]
 Andrew Tomazos Posts: 137 Registered: 8/1/05
Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 1:03 PM

Please consider the following formal proof language example:

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
thereexists m, n in N
{
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>

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