Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

You are looking at the old blog archive. LogBlog has moved to richardzach.org.

If you'd like to receive updates on new posts, please subscribe there!

Submitted by Richard Zach on Thu, 05/01/2014 - 12:16pm

- Richard Zach's blog
- Log in to post comments

The LaTeX package bussproofs.sty for typesetting natural deduction/sequent calculus proofs is nifty especially for its nice alignment of sequents. By contrast to the proof.sty package, it doesn't allow you to typeset missing parts of a proof, though. proofs.sty has the \deduce command for that; it typesets vertical dots instead of a horizontal inference line.

I wrote an add-on for bussproofs.sty that does the same. Not quite ready for prime time yet, but if you like playing with bleeding-edge stuff, you can get it here. Feedback? Please file an issue on github.

File attachments:

- Open Logic Project
- The LogBlog is Moving!
- Academic Genealogy Graphed
- CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
- In Memoriam: Grigori Mints
- Previously Unknown Turing Manuscript Going to Auction
- Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)
- Carnap on "Syntax" vs "Semantics"