Princeton University |
Computer Science 496 |
|
Note: The Twelf mode for Emacs seems to have trouble with the <!- syntax. The "check-declaration" (control-C control-D) command doesn't work on such declarations, and the fontifying may get stuck too. Instead of "check-declaration" use "check-file" (control-C control-S), and if fontifying gets stuck, just to control-G and then (control-X b) to switch to the unfontified buffer.
Second, play with it. Use the Trace facility (in the Twelf menu of the Emacs buffer) to set a breakpoint on |-break or on the rule of your choice. Then run some queries to prove some theorems. Sample queries can be found in test.elf and vctest.elf.
At a breakpoint, use the "h" command and the "g" command to print out the hypotheses and goal, respectively. Then copy these from the *twelf-server* buffer to a new file, and load that file. An example of such a file is foo.elf. In this way, you can debug the prover on individual cases.
Take some query like
%query 1 1 V : nil |- (forall2 [a][b] a and b imp b and a) by P.and run it. Examine V to see which tactics were used. Now disable one of the tactics (by commenting it out and reloading the entire prover), and run the query again. You should reach the breakpoint at |-break. (If you don't, that means some other tactic was able to prove the theorem, so examine the new V and comment out another tactic.) Now, use the "h" and "g" commands at the breakpoint to examine the state in which the commented-out tactic succeeded.
Your homework: Sometime before 10:00 a.m. Wednesday April 11th, demonstrate to the teaching assistant (Neophytos Michael) that you know how to do all these things. Make an appointment with him to do this demonstration.