winterkoninkje: shadowcrane (clean) (Default)

Until recently I've been using semantic for typesetting my deduction rules and deduction proofs. But in writing the last few papers I've become acutely aware of its limitations: in particular, it offers no way to do dotted or doubled inference lines. After looking around for a while I found bussproofs; and I don't think I'll ever look back.

The semantic package is solid enough, and follows the traditional structural/nested style of macros. At first I was quite dubious of bussproofs' stack-machine style of macros, but after typing up a few proofs in it, I'm convinced. Because you don't have all the nested braces, it's much easier to restructure, clean up, or copypaste chunks of proofs. It's a bit verbose, all told, but that's easy enough to remedy by writing your own layer of macros on top of it. The one downside to bussproofs (compared to semantic) is that it doesn't support arbitrarily many premisses, and it doesn't allow vertical orientation of premisses. So if your typing rules are complex enough, you may need to stick with semantic; but for doing proofs in basic logics, or for doing CCG derivations, bussproofs is where it's at.

This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

If you are unable to use this captcha for any reason, please contact us by email at support@dreamwidth.org

April 2019

S M T W T F S
 123456
78910111213
14151617181920
212223242526 27
282930    

Tags

Page generated 11 Jun 2025 04:26 am
Powered by Dreamwidth Studios