kpierce@ub.d.umn.edu (Keith Pierce) (02/09/91)
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:
Problem: Derive (p => t) from
(p => ((q and r) or (s and t))
and (r => t)
Proof:
1 | (p => ((q and r) or (s and t)) hypothesis
2 | (r => t) hypothesis
|-------
3 | | p hypothesis
| |------
4 | | (p => ((q and r) or (s and t)) 1, reiteration
5 | | ((q and r) or (s and t)) 3,4 modus ponens
6 | | | (q and r) hypothesis
| | |------
7 | | | r 6, conj elim
8 | | | (r => t) 2, reiteration
9 | | | t 7,8, modus ponens
| |
10 | | | (s and t) hypothesis
| | |-----
11 | | | t 10, conjunction elimination
12 | | t 5,6-9,10-11, disj. elimination
13 | (p => t) 3-12, implication introduction
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.
How would you typeset this easily in LaTeX? I can figure out how to
typeset a deduction that has no subsidiary deductions using LaTeX's
tabular environment, and probably figure out how to write a macro that
generates a line number and automatically increments it. But how about
the subsidiary deductions? The format seems to beg for a nested tabular
environment, but then (a) how do you generate the proper line numbers in
the outermost environment, and (b) how do you get the rightmost column
of proof justifications to line up correctly across all deductions?
OK, I'm willing to consider a TeX solution, but would prefer to stay
in LaTeX, or at least use TeX commands that work correctly using
lplain.tex.
Keith Pierce
Keith Pierce, Professor
Department of Computer Science
University of Minnesota, Duluth
Duluth, MN 55812-2496
internet: kpierce@d.umn.edu
bellnet: 218-726-7194sean@castle.ed.ac.uk (S Matthews) (02/09/91)
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