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 ]
 Slawomir Posts: 15 Registered: 12/8/04
Re: Formal Proof Language Example - Human-Readable?
Posted: Jun 23, 2009 2:37 PM

Yes, I can understand the meaning of the (assertion of) the theorem.
I think a good formal proof language has to have the following
features:

1. Be readable for people with general mathematical education, without
having the study the language. Readability is of course relative and
depends on the reader's experience. For some people a proof is
readable if it looks like Lisp. For most mathematicians though the
proof is readable if it looks similar to what they can see in a
standard journal. I think your syntax does have this feature.

2. Provide ways to cope with excessive verbosity. Formal proofs are
typically very verbose. A proof language should provide ways to
structure the proofs so that at least in a web presentation the reader
can choose how detailed the proof she wants to see. Your syntax is too
verbose.

3. Should support LaTeX-like mathematical symbols and notation. This
can be done by a presentation layer, but there has to be way to render
the proofs so that they look like math. This is also needed for 2.

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.

Isar is a proof language that has all these features to some extent.
<plug> See formalmath.org site for an examples </plug>.

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