winterkoninkje: Shadowcrane (Default)
[personal profile] winterkoninkje

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.

Profile

winterkoninkje: Shadowcrane (Default)
wren gayle romano

March 2014

S M T W T F S
      1
2345678
9 101112131415
16171819202122
23242526272829
3031     

Most Popular Tags

Expand Cut Tags

No cut tags

Style Credit

Page generated Apr. 17th, 2014 03:59 am
Powered by Dreamwidth Studios