-
Grégoire Lecerf
Joris van der Hoeven
Joris van der Hoeven
mailing-list for TeXmacs Users
Text archives Help
From : Andreas Seidl <address@hidden>- To: address@hidden
- Cc: Paulo Jorge de Oliveira Cantante de Matos <address@hidden>
- Subject: Logical Frameworks [Was: Interfacing texmacs with Isabelle]
- Date: Thu, 23 Oct 2003 21:59:08 +0200 (CEST)
> 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
- 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
- Logical Frameworks [Was: Interfacing texmacs with Isabelle], Andreas Seidl, 10/23/2003
Archive powered by MHonArc 2.6.19.
