New on CTAN: logicproof
Date: March 22, 2014 8:46:08 AM CET
Alan Davidson submitted the
logicproof
package.
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 http://mirror.ctan.org/macros/latex/contrib/logicproof/ This Catalogue entry does not yet exist, but we will hopefully not forget to create it: http://www.ctan.org/pkg/logicproof We are supported by the TeX Users Group http://www.tug.org . Please join a users group; see http://www.tug.org/usergroups.html .
Thanks for the upload. For the CTAN Team Petra Rübe-Pugliese
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 http://mirror.ctan.org/macros/latex/contrib/logicproof/ This Catalogue entry does not yet exist, but we will hopefully not forget to create it: http://www.ctan.org/pkg/logicproof We are supported by the TeX Users Group http://www.tug.org . Please join a users group; see http://www.tug.org/usergroups.html .
Thanks for the upload. For the CTAN Team Petra Rübe-Pugliese
logicproof – Box proofs for propositional and predicate logic
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.
The package provides environments for typesetting such proofs and boxes. It creates proofs in a style similar to that used in “Logic in Computer Science” by Huth and Ryan.
| Package | logicproof |
| Version | 2014-03-20 |
| Maintainer | Alan Davidson |