Automated Theorem Proving

1. Clause Form Algorithm
   • Old version:
     • PDF
     • HTML

   • New version:
     • PDF
     • HTML

2. Resolution Proof in Natural-Deduction Format

3. Notes on the Unification Algorithm [PDF]

4. Unification Algorithm (PDF file)

5. Unification Example (PDF file)

6. Further Thoughts on Unification

7. Another Resolution Example

8. Examples of Resolution with Answer Literals:
   1. Example 1 [PDF]
   2. Example 2 [PDF]

9. Some references:
   • Davis, Martin & Putnam, Hilary (1960) "A Computing Procedure for Quantification Theory", Journal of the ACM 7(3): 210-215.
     • Explains Skolemization and CNF.

   • Robinson, J. Alan (1965), "A Machine-Oriented Logic Based on the Resolution Principle", Communications of the ACM 12(1): 23-41.

   • Knight, Kevin (1989), "Unification: A Multidisciplinary Survey", ACM Computing Surveys 21(1): 93-124.