CR: 3
Pre-req: 249,459

Syllabus: Signature, algebra's, sub algebra's, algebraic closed systems, algebraic induction; algebraic structures: semi groups, monodies, groups, rings; homomorphisms and congruencies, term algebra's, stable congruencies, varieties and quasi varieties; signatures with predictable symbols, clauses, models, conclusions and derivation, soundness and completeness; predicate calculus, unpredictability, Skolem normal forms; clauses with variables, resolution principle.

Outline:

1. Propositional Logic

Introduction
Validity & Inconsistency
Normal forms in propositional logic
Logical consequences
Applications
2. First-order Predicate Logic

Introduction
Prenex normal form in FOL
Applications
3. Herbrand Theorem

Introduction
Skolem standard forms
Herbrand Universe and Base
Herbrand Theorem
4. Resolution Principal

Introduction
Resolution in Propositional Logic
Substitution & Unification
Resolution in First-order Logic
Completeness of resolution principal
Lifting Lemma
Examples
Deletion strategy: subsumption
5. Semantic Resolution & Lock resolution

Introduction
Semantic trees
Ordering in semantic resolution
Hyper-resolution
Lock resolution
Completeness of lock resolution
6. Linear Resolution

Introduction
Input resolution and Unit resolution
Completeness of linear resolution
Linear deduction and tree searching
BFS
DFS
Heuristics in Tree Searching
7. Equality Relation

Introduction
Demodulation
Paramodulation
Hyper-paramodulation
8. Proof Procedures Based on Herbrand's Theorem

Examples of theorems are chosen from the following domains: Number Theory, Set Theory, Algebraic structures such as semi groups, monodies, groups, rings, lattices; Homomorphisms and Congruencies.

Textbook: Symbolic Logic and Mechanical Theorem Proving
                  Chang & Lee
                  Academic Press Publishing Company

Additional References:
                  - The Great Theorem Prover
                    Newborn Software Publishing

Course Important Links:
    * Assignments page
    * Almulla's paper on Number Theory

Theorem Provers Used in This Course:
    * Otter
    * Theo: Given in class.
    * Herby: Given in class.