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 ]
 Charlie-Boo Posts: 1,635 Registered: 2/27/06
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 21, 2009 9:14 PM

On Jun 21, 1:03 pm, Andrew Tomazos <and...@tomazos.com> wrote:
> 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.

This seems to be in 1-to-1 correspondance with FOL plus some noise
words. So the only difference is the syntax used, which is
immaterial.

C-B

> Thanks,
> Andrew.
>
> --
> Andrew Tomazos <and...@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