Exercises 8.3, 8.4, p. 147 of Thompson.
Exercises 14.22, 14.23, page 256 of Thompson. (Type NTree is defined at the bottom of page 251.)
Exercises 14.37, p. 264 of Thompson.
Exercises 17.22, 17.24, pages 369, 370 of Thompson.
Exercises 18.5, 18.7, p. 395 of Thompson.
What is the definition of a Horn sequent? Why are Horn sequents used in logic programming instead of allowing arbitrary sequents as axioms?
If you unify formula p(X,q(a),W) with p(r(Z),W,V), where X, W, V and Z are variables, what variable substitutions will be needed, and what formula results from doing the unifying substitution?