Automated Theorem Proving: Course Content
Introduction
What is ATP?
Logical Consequence
Logical Consequence by Truth Tables
1st order logic
The Language
Logical Consequence by SPTs
Clause Normal Form
The Herbrand World
The Resolution Inference Rule
The CNF Saturation Procedure
The ANL Loop
Equality Reasoning
Paramodulation
Superposition