Automated Theorem Proving : Coq, Vampire, Z3 - Three very different approaches!
Coq is a powerful proof assistant for higher-order logic, Vampire is the CADE champion resolution theorem prover, Z3 is an SMT solver developed at Microsoft Research that uses efficient decision procedures. It is used for many practic al applications, especially in program analysis.
The primary goal of this course is to develop a working knowledge of Coq. We will cover Z3 and Vampire as time permits according to student interest. However each of these could take a full semester by itself.