The cited references can be found in the Readings section.
| Date | Topics | Readings |
|---|---|---|
| 01/20/04 |
Introduction and syllabus overview. Discussion of several forms of reasoning (deductive, inductive, abductive, probabilistic, and so on). The automation of deductive reasoning and its applications in computer science. Mathematical logic as a foundation for automated deduction. Brief survey of various logics and their use in computer science. Motivation for concentrating on first-order classical logic. |
- Chap. 1,2 of [SocJoh]
- [Por01] (optional) |
| 01/22/04 | The language of first-order logic. Signatures, terms, logical connectives, quantifiers, formulas. The principle of structural induction (for terms and for formulas). Examples of simple proofs by structural induction. Free and bound variables of a formula. |
Chap. 3 of [SocJoh]
|
| 01/27/04 | Semantics of first-order logic. Ontological commitments. Structures, valuations and interpretations. Examples of interpretations. The satisfiability relation between interpretations and formulas. Validity. |
Chap. 4 of [SocJoh]
|
| 01/29/04 | Example of interpretation and formulas that are satisfiable, unsatisfiable or valid in the interpretation. The logical entailment relation between sets of formulas and formulas. The Deduction Theorem. Discussion on how the entailment relation is semi-decidable but impractical to check directly. The need for a more syntactical characterization of entailment: provability. Substitutions. |
Chap. 4 of [SocJoh]
|
| 02/03/04 | Extension of substitutions from terms to formulas. The problem of capturing. Examples. Composition of substitutions. Associativity and identity of the composition of substitutions over terms. Non associativity of composition over formulas. Rectified formulas. Idempotent substitutions, definition and characterization. Renaming substitutions, definition and characterization. |
Sec. 3.4 of [SocJoh]
|
| 02/05/04 |
The Substitution Lemma.
Significance and proof.
Some consequences of the lemma.
Examples. Inference systems (calculi). General definition as a pair of axioms and derivation rules. Rules as non-deterministic, computable functions from sets of formulas to sets of formulas. General definition of derivation as a sequence of sets of formulas. Notions of proofs and probability in an inference system. Idea of soundness and completeness. |
Chap. 4 of [SocJoh]
|
| 02/10/04 | The Gentzen Calculus. Sequents, axioms and derivation rules. Satisfiability and validity of sequents. Soundness of derivation rules. Derivations trees, proof trees and provability. Top-down versus bottom up generations of derivation trees. Soundness of the calculus: every provable formula is valid. Proof of soundness. Completeness and decidability issues. Discussion on the semi-decidability of validity first-order logic and on the decidability of validity for restricted classes of first-order formulas. |
Sec. 5.1 of [SocJoh]
|
02/12/04 | The Herbrand universe for a set of formulas. The set Gamma^{infinity} of persistent formulas in a sequence Gamma_0, Gamma_1, ... Fair derivation trees in G. Discussion on the existence of algorithms for generating fair derivation trees. Closure properties of infinite branches in fair derivation trees. |
Sec. 5.2 of [SocJoh]
|
02/17/04 | Herbrand structures and Herbrand interpretations. Example of Herbrand structure. Proof of completeness of the Gentzen Calculus. Fix to incorrect incompleteness proof in the textbook. |
Sec. 5.2 of [SocJoh]
|
02/19/04 | Decidability of the validity of universal formulas. Proof using the Gentzen calculus. Discussion on why the Gentzen calculus is not adequate for automated reasoning. Introduction to refutation-based calculi and to clause normal form. Conversion of arbitrary formulas into clause normal form. Skolemization. Clauses and clause sets. Satisfiability of clauses versus the satisfiability of quantifier-free formulas. Intuitions on why it is easier to check for unsatisfiability of clauses than for the validity of arbitrary formulas. The unification mechanism. Brief preview of the resolution calculus and the ideas behind it. |
Sec. 5.2 and 7.1 of [SocJoh]
Class notes from 145. |
02/24/04 | Unifiers. Motivating examples. Term equations, systems of equations and their unifiers. Systems in solved form. Bijective correspondence between systems in solved form and idempotent substitutions. Most general unifier of a system. Various properties of systems in solved form and their most general unifiers. Inference rules for computing a most general unifier of a system of equations. |
Sec. 7.2 of [SocJoh]
|
02/26/04 | Example of computing most general unifiers with the unification inference rules. Proof of termination and correctness of the unification rules. |
Sec. 7.2 of [SocJoh]
|
03/02/04 | Discussion on midterm projects. The resolution calculus: introduction and motivation. Detecting unsatisfiability by computing most general unifiers. Sequent notation for clauses. The resolution rule and the factoring rules. Examples of rule applications. Tautological clauses, definition and characterization. |
Sec. 7.4 of [SocJoh]
|
03/04/04 | Ground and non-ground subsumption, definition and characterization. Examples of subsumed clauses. Redundant clauses. The inference system R, the deduction and the reduction rule. Derivations and refutations in R. Proof of soundness of R. |
Sec. 7.4 of [SocJoh]
|
03/09/04 | Completion of soundness proof for the inference system R. Proof of completeness of R. |
Sec. 7.4 of [SocJoh]
|
03/11/04 | Completion of completeness proof for R. |
Sec. 7.4 of [SocJoh]
|
03/16/04 | Spring break. | 03/19/04 | Spring break. | 03/23/04 | Fair derivations strategies. Level saturation and Level saturation with solution. Example of derivation. Preference strategy with evaluation functions. Fairness/completeness issues. Example of unfair and incomplete strategy. |
Sec. 7.5 of [SocJoh]
|
03/25/04 | Improving the deduction efficiency of the resolution calculus. Delying unification. Clauses with unification constraints. A constraint version of the resolution calculus R. Derivation strategies. Unit resolution and input resolution. Incompleteness and refutation equivalence of the two strategies. Completeness of unit resolution for Horn clauses. Examples. |
Sec. 8.1-8.3 of [SocJoh]
|
03/30/04 |
Student presentations:
Advanced Indexing Operations on Substitution Trees, by Peter Graf and Christoph Meyer. Computing Small Clause Normal Forms, by Andreas Nonnengart and Christoph Weidenbach. Tableaux and related methods, by Reiner Hähnle. |
Presented papers | 04/01/04 |
Student presentations:
Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux, by Reinhold Letz and Gernot Stenz. Theorem Proving via General Matings, by Peter B. Andrews. |
Presented papers | 04/06/04 |
Student presentations:
Limited Resource Strategy in Resolution Theorem Proving, by Alexander Riazanov and Andrei Voronkov. Resolution in Sorted Logics, by Rolf Socher-Ambrosius and Patricia Johann. New Directions in Instantiation-Based Theorem Proving, by Harald Ganzinger and Konstantin Korovin. |
Presented papers | 04/08/04 |
Student presentations:
Model Elimination Without Contrapositives and Its Application to PTTP, by Peter Baumgartner and Ulrich Furbach. Efficient Instance Retrieval with Standard and Relational Path Indexing, by Alexandre Riazanov and Andrei Voronkov. |
Presented papers | 04/13/04 | Discussion on final projects. More derivation strategies for the resolution calculus. Linear resolution. Examples. Completeness of linear resolution. Hyperresolution. |
Sec. 8.4-8.5 of [SocJoh]
|
04/15/04 | Semantic Resolution strategy and Set of Support strategy. Comparisons between the two. Completeness of set of support. Examples of applications of semantic resolution and of set of support. |
Sec. 8.6 of [SocJoh]
|
04/20/04 | Resolution with selection function. Examples of selection functions. Completeness of resolution with selection function. Discussion of selected problems from Homework 2. |
Sec. 8.7 of [SocJoh]
|
04/22/04 | Ordered Resolution. A general notion of redundancy based on term orderings. The inference system O^> and its reduction rule. Notion of redundancy in inference system R and reduction rule in R as special cases of notion of redundancy in O^> and reduction rule in O^>. Level saturation with immediate solution in O^>: an example. |
Sec. 8.8 of [SocJoh]
|
04/27/04 | The Model Evolution Calculus. Motivation and overview. The DPLL procedure. Example. The DPLL calculus, contexts and clause sets, and interpretations induced by a context. A model evolution view of the DPLL calculus. Lifting the DPLL procedure to the first-order level. The notion of permanent satisfiability. First-order contexts. |
[BauTin03] from the Readings section.
|