15-815 Automated Theorem Proving
Fall 1999
Frank Pfenning

Sample propositional focusing provers in ML

prop.sml - Propositions
ctx.sml  - Contexts
prover.sig - Prover interface
focus1.sml - Focusing prover using search combinators (tacticals)
focus2.sml - Focusing prover using success continuations directly
focus3.sml - Focusing prover using boolean return values

test.sml - Some test cases
