mailing-list for TeXmacs Users

[Andreas Seidl <address@hidden>]

>   1) Write parsers and pretty printers for sufficiently customizable
>      mathematical grammars.

Does this mean "MathML"?

> 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/

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. 

andreas.

Departmento de Matematicas, Estadistica y Computacion
Facultad de Ciencias, Universidad de Cantabria
Avda. de Los Castros s/n
39006 Santander
Spain
Phone: +34 942 201 360
Fax: +34 942 201 402