LaTeX for your logic homework

It’s been a long time since I’ve posted. Day job has taken over my life. It’s had me attached to a keyboard working 12 hour days for pretty much a month now. I haven’t had much chance or desire to geek out after getting home from work as a result.

With the fall semester starting up (my last class!) I have spent some time playing with LaTeX again. I’ve been using LaTeX off and on for a few years to prepare labs and reports for school and even some proposals for work though I’ve never done more than minor edits to existing LaTeX styles. For my fall class I’m using LaTeX in a similar capacity but with a fun twist: I’m formatting propositional logic proofs.

First off the class is CSE 774: Access Control, Security, and Trust taught by Dr. Shiu-Kai Chin at Syracuse University. He co-authored a boot by the same name if you’re interested in the content. Long story short Dr. Chin and Dr. Older developed a small logic language based on the logic of Abadi and Lampson. They use their logic to formally reason about access control decisions in a number of systems. Interesting stuff.

Most of the homework I’ve been doing requires either doing formal proofs or manipulating formulas and constructing Kripke Structures. The first assignment got messy quick so instead of copying all of my work over I decided I’d type it up in LaTeX. I managed to use generic math mode (the align environment) for most of my work but the structured proofs needed something extra.

Thankfully some industrious academics out there ran into this problem long ago and wrote two different styles for typesetting Fitch-style structured deduction. Both have their strengths and in the end I used a mix of the two. The fitch style is simple and straight forward. That said I couldn’t figure out a way to get it to display multi-line formulas which was a problem since the logic we’re using is quite verbose. I managed to track down another fitch style, this one by Peter Selinger which handles multi-line formulas quite well.

I know people are always looking for a way to get their work done more quickly and LaTeX isn’t going to help you there. So in the end my homework didn’t get done any faster but it sure looked nice when I was done 🙂