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:51 AM

On Jun 23, 8:37 pm, slawekk <skoko...@yahoo.com> wrote:
> 4. Should support some notion of context to be able to limit the scope
> of introduced notation, independent of the defined notions. For
> example you should be able to talk about groups using both
> multiplicative and additive notation (in different contexts), or use
> the same \cdot symbol to denote both general group operation and
> multiplication of real numbers (again in different contexts). How
> important this need is becomes obvious only when you reach certain
> scale.

In this example the NaturalNumbers set (which is imported from
edu.mit.natural_number) introduces meaning to the various functions:

x^y
x + y
x = y
x, y are_relative_prime
x is odd
x <= y
x - y
2
x * y

where x and y are NaturalNumbers.

This mechanism functions in the same way as overload resolution does
in C++ - and when you think about it - this is the same way humans
infer what a function means. If I say:

<some_operand_a> <some_operator> <some_operand_b>

Then you mentally search all the known operators that look like
"some_operator" to the type of thing that "some_operand_a" and
"some_operand_b" represent. There can however be multiple different
operators that look exactly like some_operator.
-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