New on CTAN: logicproof

CTAN Announcements ctan-ann at
Sat Mar 22 08:46:08 CET 2014

Alan Davidson submitted the



Version date: 2014/03/20
License type: lppl

Summary description: Box proofs for propositional and predicate logic

Announcement text:

 First public release

 A common style of proof used in propositional and predicate
 logic is Fitch proofs, in which each line of the proof has a
 statement and a justification, and subproofs within a larger
 proof have boxes around them.  This package provides
 environments for making such proofs and boxes. It creates
 proofs in a style similar to the one used in "Logic in Computer
 Science" by Huth and Ryan.

 When I took a logic class in college, the professor lamented
 that there wasn't a good way to make these box proofs in LaTeX,
 and suggested that the class write up their assignments in
 LaTeX without boxes, print them out, and draw the boxes in by
 hand before turning them in. Unsatisfied with this approach, I
 created some macros to draw these boxes in LaTeX itself. I
 shared that code with the professor, who liked it enough to
 share it with the rest of the class.

 It's been nearly a decade since then, and I have recently
 discovered that not only are people still using my old code,
 its use has spread to other colleges. I had assumed that in the
 intervening time, a professional logician would have made and
 published a better implementation, but that doesn't seem to
 have happened. This is an improved version of my old code, with
 several problems fixed and a more standardized syntax.


This package is located at

This Catalogue entry does not yet exist, but we will hopefully
not forget to create it:

We are supported by the TeX Users Group .  
Please join a users group; see .


   Thanks for the upload.

     For the CTAN Team
    Petra RĂ¼be-Pugliese

More information about the Ctan-ann mailing list