Chronological Thread 

< Chronological >      < Thread >

---

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.

---

• Interfacing texmacs with Isabelle, Paulo Jorge de Oliveira Cantante de Matos, 10/23/2003
  • Re: [TeXmacs] Interfacing texmacs with Isabelle, Bas Spitters, 10/23/2003
  • Re: [TeXmacs] Interfacing texmacs with Isabelle, Joris van der Hoeven, 10/23/2003
    • Logical Frameworks [Was: Interfacing texmacs with Isabelle], Andreas Seidl, 10/23/2003
      • Re: [TeXmacs] Logical Frameworks [Was: Interfacing texmacs with Isabelle], Joris van der Hoeven, 10/24/2003

---

Archive powered by MHonArc 2.6.19.