Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!usc!cs.utexas.edu!uunet!mcsun!ukc!edcastle!sean
From: sean@castle.ed.ac.uk (S Matthews)
Newsgroups: comp.text.tex
Subject: Re: Typesetting Proofs from Formal Logic
Message-ID: <8386@castle.ed.ac.uk>
Date: 9 Feb 91 13:10:02 GMT
References: <874@ub.d.umn.edu>
Organization: Edinburgh University Computer Services
Lines: 33

kpierce@ub.d.umn.edu (Keith Pierce) writes:

>I would like to typeset logical deductions in a format similar to that
>displayed in the text SYMBOLIC LOGIC, by R. H. Thomason.  The deductions
>look something like this approximation using ASCII text:

>For those not familiar with the notation: the vertical lines represent
>deductions, the horizontal line separates hypotheses for the deduction
>from derivations that use the hypotheses.  One can nest subsidiary
>deductions, in which temporary hypotheses are made and then dispatched
>using the usual Gentzen-type natural deduction rules.

>Keith Pierce

I think the vertical lines would make the text very cluttered, but apart
from that...

Have you tried Mario Woczko's macro package for setting VDM text---there
are very good (and good looking) facilities in that for setting Natural
Deduction proofs in pretty much the way that you asked for here (without
the lines---but I do not think it would not be hard to hack lines in if
you really insisted on them). 

The National Physical Laboratory has another set of VDM macros that do
the same thing, only better---but they are enormous (they are designed,
after all, for setting formal specs, not logic exercises).

try Mario Wolczko: mario@uk.ac.man.cs.r5
or (for the NPL macros): gip@seg.npl.co.uk <Graeme I. Parkin>

If these fail, I could mail them to you.

Sean