# New on CTAN: log­icproof

Date: March 22, 2014 8:46:08 AM CET
Alan David­son sub­mit­ted the log­icproof pack­age. Ver­sion date: 2014/03/20 Li­cense type: lppl Sum­mary de­scrip­tion: Box proofs for propo­si­tional and pred­i­cate logic An­nounce­ment text:
First pub­lic re­lease A com­mon style of proof used in propo­si­tional and pred­i­cate logic is Fitch proofs, in which each line of the proof has a state­ment and a jus­ti­fi­ca­tion, and sub­proofs within a larger proof have boxes around them. This pack­age pro­vides en­vi­ron­ments for mak­ing such proofs and boxes. It cre­ates proofs in a style sim­i­lar to the one used in "Logic in Com­puter Science" by Huth and Ryan. When I took a logic class in col­lege, the pro­fes­sor lamented that there wasn't a good way to make these box proofs in LaTeX, and sug­gested that the class write up their as­sign­ments in LaTeX with­out boxes, print them out, and draw the boxes in by hand be­fore turn­ing them in. Un­sat­is­fied with this ap­proach, I cre­ated some macros to draw these boxes in LaTeX it­self. I shared that code with the pro­fes­sor, who liked it enough to share it with the rest of the class. It's been nearly a decade since then, and I have re­cently dis­cov­ered that not only are peo­ple still us­ing my old code, its use has spread to other col­leges. I had as­sumed that in the in­ter­ven­ing time, a pro­fes­sional lo­gi­cian would have made and pub­lished a bet­ter im­ple­men­ta­tion, but that doesn't seem to have hap­pened. This is an im­proved ver­sion of my old code, with sev­eral prob­lems fixed and a more stan­dard­ized syn­tax.
This pack­age is lo­cated at http://mir­ror.ctan.org/macros/la­tex/con­trib/log­icproof/ This Cat­a­logue en­try does not yet ex­ist, but we will hope­fully not for­get to cre­ate it: http://www.ctan.org/pkg/log­icproof We are sup­ported by the TeX Users Group http://www.tug.org . Please join a users group; see http://www.tug.org/user­groups.html .
Thanks for the up­load. For the CTAN Team Pe­tra Rübe-Pugliese

## log­icproof – Box proofs for propo­si­tional and pred­i­cate logic

A com­mon style of proof used in propo­si­tional and pred­i­cate logic is Fitch proofs, in which each line of the proof has a state­ment and a jus­ti­fi­ca­tion, and sub­proofs within a larger proof have boxes around them.

The pack­age pro­vides en­vi­ron­ments for type­set­ting such proofs and boxes. It cre­ates proofs in a style sim­i­lar to that used in “Logic in Com­puter Science” by Huth and Ryan.

 Pack­age log­icproof Ver­sion 2014-03-20 Main­tainer Alan David­son

more