There are a lot of exercises, so if you have your own proofs/programs
/proofs-as-programs
/corrections, feel free to submit a pull request.
Note: Gallier writes (f ∘ g)(x) to mean g(f(x)).
Solutions for Logic for Computer Science: Foundations of Automatic Theorem Proving (2nd ed)
TeX