Automated Theorem Proving
Spring Semester, 2006
General information
Home Exam An Important Note: We decided to simplify the exam by
allowing two arbitrary questions to be optional. Also, students which did not
summarize one class are requested to complete one more question.
Bibliography
- A. Avron, Gentzen-Type Systems, Resolution and Tableaux Journal of Automated Reasoning 10, 265-281 (1993)
- Wos, Overbeek, Lusk,
Boyle Automated Reasoning:
Introduction and applications
- A.
Robinson and A. Voronkov (ed.) Handbook of Automated Reasoning, vol.
1-2
- M.
Fitting, First-Order Logic and
Automated Theorem Proving
- Computational
Logic Course (Stanford)
- Demillo,
Lipton, and Perlis, Social
Processes and Proofs of Theorems and Programs, CACM 79
- J Strother
Moore, A
Mechanized Program Verifier, talk at The Verification Grand
Challenge Workshop, Zurich,
October 10--13, 2005
- The
verifying compiler challenge, Tony Hoare, JACM
- W.H. Joyner Jr. Resolution. Strategies as Decision
Procedures. Journal of the ACM, 23(3):398-417, 1976.
- L. Bachmair
and A. Tiwari. Abstract congruence closure and
specializations. In D.A. McAllester, editor, Proceedings
of the 17th International Conference on Automated Deduction, volume
1831 of LNAI, pages 64-78. Springer-Verlag,
2000.
- G.
Nelson and D.C. Oppen. Fast decision procedures
based on congruence closure. Journal of the ACM, 27(2):356-364,
1980.
- G. Nelson and D.C. Oppen. Simplification by cooperating decision
procedures. ACM Transactions on Programming Languages and Systems,
1(2):243-257, 1979.
- F. Baader and K.U.
Schulz. Unification in the union of disjoint equational
theories: combining decision procedures. Journal of Symbolic
Computation, 21(2):211-243, 1996.
- Mini
Sat
Homework assignments