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 --------------------------- For the assignment: 1) You can run the code by CM.make' ("dyck.cm"); This is just because we do not use the default sources.cm make file. CM.Make' allows you to pass files with different names to ML's compilation manager. 2) You need to implement dyck.sml Pick one of the focusing prover implementations and modify it -- this code should go to file dyck.sml.