Homework Assignment 4
Due Tue Feb 17

The goal of this assignment is to modify the interactive theorem prover
from assignment 3 to account for existential variables (to resolve
universal and existential non-determinism) and occurrence variables (to
resolve resource non-determinism).

You are given a modified specification (term.sig) and implementation
(term.fun) of terms which permit existential variables and implement
unification with an extended occurs-check.

You are asked to:

0. Debug term.sig and term.fun if necessary.  Please let me know if
   you find a bug so I can post this information on the course
   home page.

1. Modify the signature SEQ in file seq.sig to account for occurrence
   variables.

2. Implement the sequents with occurrence variables in file seq.fun.

3. Modify your implementation of rules.fun from assignment 3 to account
   for existential and occurrence variables.  The new implementation
   should satisfy the given signature rules.sig.  Note that an attempt
   to illegally apply a rule should not have an side-effect on the
   state.

4. Modify top.fun so the goal sequents are set up properly when
   Top.prove or Top.entail are called.

5. Use the new implementation to prove
   a.  (exists x. (P(x) -o Q)) -o ((forall x. P(x)) -o Q)
   b.  (A -o (B -o C)) -o ((A * B) -o C)

6. Demonstrate one attempt each to prove
   a.  ((forall x. P(x)) -o Q) -o (exists x. (P(x) -o Q))
   b.  ((A & B) -o C) -o (A -o (B -o C))
   which fails due to unsatisfiable unification problems
   or occurrence constraints.


EXTRA CREDIT:

Present an abstract version of your occurrence constraint manipulation
algorithm and prove it correct.