From: Szabolcs Nagy <nszabolcs_AT_gmail.com>

Date: Sat, 3 Oct 2009 18:30:53 +0200

Date: Sat, 3 Oct 2009 18:30:53 +0200

On 10/3/09, markus schnalke <meillo_AT_marmaro.de> wrote:

*>> otoh it would be nice if maths had a plain text representation with a
*

*>> proper formal language, well defined scoping rules, semantics.. and if
*

*>> one came up with a new construct he would define it inside the
*

*>> language
*

*>
*

*> Reminds me much of `eqn', which AFAIK provides all of this.
*

*>
*

no, i was thinking about a bit different thing there

in eqn one cannot define axioms which later could be used for formula

correctness verification

eqn is good for typesetting formulas, but it's not good as

mathematical notation for the digital age. it is important to be able

to express the semantic meaning behind the symbols.

a good language would make the processing of the formulas possible

(static analysis to catch errors, search for certain

constructs/patterns, evaluate formulas, describe proofs in a

verifiable way, render formulas nicely..)

coq, isabelle, mizar, metamath, acl2, agda.. is closer what i was thinking

Received on Sat Oct 03 2009 - 16:30:53 UTC

*
This archive was generated by hypermail 2.2.0
: Sat Oct 03 2009 - 16:36:01 UTC
*