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
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 24, 2009 11:35 AM

On Jun 24, 9:46 am, Tim Smith <reply_in_gr...@mouse-potato.com> wrote:
> In article
>  Spiros Bousbouras <spi...@gmail.com> wrote:
>

> > 3) I don't like that you are using ";" for conjunction. The
> >    established term is "and" and I see no reason to change it.
> >    Since I also do programming I can live with & or && but not ;.

>
> He doesn't appear to be using ";" for conjunction. He's using it for
> statement termination, like a period in written English. If he were
> using it for conjunction, the last line in each group would not end with
> ";".

Actually the ";" is just a carriage return replacement to make
whitespace insignificant. The form is just as a seperator between
items in some list. In Python-style with significant whitespace this
would look like:

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

Which some may prefer. The "{;;;}" just adds an extra layer of safety
(a cross-check).
-Andrew.

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