First login?
Lost password?
 
 
 
mailing-list for TeXmacs Users

Text archives Help


Re: [TeXmacs] Natural Deduction


Chronological Thread 
  • From: Henri Lesourd <address@hidden>
  • To: Joris van der Hoeven <address@hidden>
  • Cc: address@hidden
  • Subject: Re: [TeXmacs] Natural Deduction
  • Date: Fri, 21 Oct 2005 22:39:37 +0200


Joris van der Hoeven wrote:

On Fri, Oct 21, 2005 at 09:50:52PM +0200, Henri Lesourd wrote:

On 10/15/05, Henri Lesourd <address@hidden> wrote:

I want to typeset some Natural Deduction proofs in TeXmacs. See pages
15 and 16 of [1] for some examples and the formal syntax. Using
faction bars almost works. The only problem is that they extend their
width to include everything above and below them. For natural
deduction the bar should only extend to include the things immediately
above and below. Does there exists a TeXmacs module for this or how
would I go about typesetting this?

The plugin is now available on my web page :
<<
http://www.ags.uni-sb.de/~henri/texmacs


The plug-in is interesting, but I do not think that it answers
the typographic question raised by Michael.

Currently, this plugin draws exactly the kind of trees that
are shown in Michael's example document. And it does that
in a completely automatic way.

The cleanest way to
implement natural deduction proofs is probably to enlarge the number
of "styles" for trees. This is an old item on the wish-list.


As you just said, the item is old... and it is old because nobody
found the courage (and/or the time) to dive in the C++ to implement
this enlargment.

And also, the code of this plugin can be changed & reused by
other people for their own purposes (draw their own kind of
trees, or do similar editors for other things). This is definitely
irrealistic to imagine this in the case of the C++.


Archive powered by MHonArc 2.6.19.

Top of page