mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Thu, 23 Oct 2003, Andreas Seidl wrote:
> >   1) Write parsers and pretty printers for sufficiently customizable
> >      mathematical grammars.
>
> Does this mean "MathML"?

This should mean "content MathML" and probably "Openmath".
As to, "presentation MathML", that should be done by David Allouche.

> > Of course, any help and suggestions are welcome. In any case,
> > if the question is whether it is possible and whether we want to support
> > logical frameworks and whether, then the answer is definitely: yes.
>
> Coq and Isabelle seem to be proof assistants for higher-order logic. The
> system I'm working with, REDLOG, is for first-order logic with fixed
> languages and theories (including propositional calculus). I've done
> some prettyprinting recently, as can be seen in two screenshots and some
> example slides (done with texmacs) at
> http://www.fmi.uni-passau.de/~seidl/software/

Seems nice! Notice that we may include improvements for the reduce plugin
directly into TeXmacs if you wish (in that case you should contact Andrey
Grozin too: address@hidden).

> maybe there are some points where this first-order stuff overlaps with the
> theorem-proving stuff; in this case it would be nice if progress was made
> not too secretly.

You may all suscribe to texmacs-dev and we can discuss technical details 
there.