- Search in the proof domain
- natural deduction
- sequents
- resolution
- Search in the semantic domain
- DPLL
- using SAT solvers incrementally

- P. C. Gilmore, A Proof Method for Quantification Theory: Its justification and Realization, IBM Journal of Research and Development, 1960
- Cormac Flanagan, Rajeev Goshi, Xinming Ou, and James B. Saxe, Theorem Proving using Lazy Proof Explication, CAV 03

- Quantifiers
- Skolemization
- Unification
- Matching
- David Detlefs, Greg Nelson and James B. Saxe, Simplify: a Theorem Prover for Program Checking, Journal of the ACM 52(3):365 - 473, 2005
- David Detlefs, Greg Nelson and James B. Saxe, Simplify: a Theorem Prover for Program Checking, Technical Report, HP Labs

- Induction
- induction
based on recursive structure
- Boyer and Moore,
*A computational logic*, Academic Press, 1979, chapter XIV - Matt Kaufmann, Panagiotis Manolios, and J Strother Moore,
*Computer-Aided Reasoning: An Approach*, Kluwer Academic Publishers, June, 2000.

- Boyer and Moore,
- inductionless induction

- induction
based on recursive structure
- Equality
- Congruence closure/E-graph
- Rewrite rules

- ESC/Java
- Flanagan, Leino, Lillibridge, Nelson, Saxe, State, Extended Static Checking for Java, PLDI 02 (read sections 1, 2, and 3)

- Rhodium
- Lerner, Millstein, Rice, Chambers, Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, POPL 05 (sections 1, 2, and 3)

- Predicate abstraction
- Susanne Graf and Hassen Saidi, Construction of Abstract State Graphs of Infinite Systems with PVS, CAV 97
- Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani, Automatic Predicate Abstraction of C Programs, PLDI 01

- Proof carrying code
- Curry-Howard isomorphism
- Gurevich, Platonism, Constructivism, and Computer Proofs vs. Proofs by Hand (handout will be given in class, with the sections you should read)