literate-unitb-logic OS X / Linux: Windows: Backend prover for doing predicate calculus with sequent calculus proofs