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