Resolution, Rewriting, Decision Procedures (to be elaborated)
Instructors: Madhavan Mukund (MM), MK Srivas (MKS), SP Suresh (SPS)
Guest lectures:, Deepak Kapur
Mathematical Logic for Computer Science, Mordechai Ben-Ari, Springer (2nd edition)
Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press
Paramodulation-based Theorem Proving, Robert Nieuwenhuis and Albert Rubio, in Handbook of Automated Reasoning, Volume 1, edited by Alan Robinson and Andrei Voronkov.
Induction and Decision Procedures, Deepak Kapur, Jürgen Giesl and Mahadevan Subramaniam, Rev. R. Acad. Cien. Serie A. Mat., Vol 98 (1), 2004, pp. 153-180.
What's so Special About Kruskal's Theorem and the Ordinal Γ_{0}? A Survey of Some Results in Proof Theory, Jean Gallier, Annals of Pure and Applied Logic, 53 (1991), 199-260.
Decision Procedures: An Algorithmic Point of View, Daniel Kroening and Ofer Strichman, Springer
GRASP: A Search Algorithm for Propositional Satisfiability, João P. Marques-Silva and Karem A. Sakallah, IEEE Transactions on Computers, 48 (1999), 506-521.
Chaff: Engineering an Efficient SAT Solver, Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik Proc 38th Design Automation Conference, DAC 2001, ACM (2001), 530-535.
An Introduction to Binary Decision Diagrams, Henrik Reif Andersen, Lecture notes, ITU Copenhagen, 1999.
Boolean Satisfiability with Transitivity Constraints Randal E. Bryant and Miroslav N. Velev, CAV 2000, Springer LNCS 1855 (2000), 85-98.
Yet Another Decision Procedure for Equality Logic, Orly Meir and Ofer Strichman, CAV 2005, Springer LNCS 3576 (2005), 112-124.
Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic, Mirron Rozanov and Ofer Strichman ENTCS 198(2) (2008), 3-17.
The Omega Test: a fast and practical integer programming algorithm for dependence analysis, William Pugh.
Lecture 1, 16 Jan 2014 (MM)
Review of propositional logic syntax and semantics, CNF, the resolution rule (Ben-Ari, Chapter 4.1)
Lecture 2, 21 Jan 2014 (MM)
Soundness and completeness of propositional resolution, review of first-order logic syntax and semantics (Ben-Ari, Chapter 4.1)
Lecture 3, 23 Jan 2014 (MM)
Clausal form, Skolemization, unification algorithm (Ben-Ari, Chapter 7.1–7.3, 7.5–7.7)
Lecture 4, 28 Jan 2014 (MM)
Unification algorithm, first order resolution (Ben-Ari, Chapter 7.7–7.8)
Lecture 5, 30 Jan 2014 (MM)
Abstract reduction systems: Equivalence and reduction, well-founded induction, proving termination, lexicographic orders (Baader and Nipkow, Chapter 2.1–2.4)
Lecture 6, 4 Feb 2014 (MM)
Lexicographic orders, multiset orders, proving confluence (Baader and Nipkow, Chapter 2.4–2.5, 2.7)
Lecture 7, 6 Feb 2014 (MM)
Terms, substitutions and identities (Baader and Nipkow, Chapter 3.1)
Deciding ≈_{E}, term rewriting systems, unification (Baader and Nipkow, Chapter 4.1–4.2,4.5–4.6)
Termination for term rewriting systems (Baader and Nipkow, Chapter 5.1 — undecidability proof to be done in detail later)
Lecture 8, 7 Feb 2014 (MM)
Reduction orders, the interpretation method, polynomial interpretations, simplification orders (Baader and Nipkow, Chapter 5.2–5.4 — many details, including proof of Kruskal's Theorem, to be done in detail later)
Lecture 9, 11 Feb 2014 (MM)
Simplification orders: recursive path orders (lexicographic order), Knuth-Bendix order (Baader and Nipkow, Chapter 5.4)
Confluence: the decision problem, critical pairs (Baader and Nipkow, Chapter 6.1–6.2)
Completion: the basic completion procedure (Baader and Nipkow, Chapter 7.1)
Many proofs omitted in the above, to be done in detail later.
Lecture 10, 12 Feb 2014 (Deepak Kapur)
Three examples involving completion
Lecture 11, 13 Feb 2014 (Deepak Kapur)
Clarification on lex ordering on strings
Formal definition of superposition
Discovering a canonical rewrite system through completion
Semi-decision procedure for t = t',
Superposition calculus
Lecture 12, 18 Feb 2014 (Deepak Kapur)
Proving properties for inductively defined datatypes via term rewriting ("inductionless induction")
Lecture 13, 20 Feb 2014 (SPS)
Undecidability of termination for term rewriting systems (Baader and Nipkow, Chapter 5.1)
Lecture 14, 04 Mar 2014 (SPS)
Polynomial intepretations and their limitations in terms of deriviation length (Baader and Nipkow, Chapter 5.3)
Simplification orderings: well-quasi orderings, Dickson's Theorem, Higman's Theorem (Baader and Nipkow, Chapter 5.4, Gallier paper Sections 2 and 3)
Lecture 15, 06 Mar 2014 (SPS)
Higman's Theorem (Gallier paper Section 3)
Kruskal's Tree Theorem (Baader and Nipkow, Chapter 5.4)
Lecture 16, 13 Mar 2014 (SPS)
Recursive path orderings (Baader and Nipkow, Chapter 5.4.2)
Lecture 17, 18 Mar 2014 (MKS) (Slides)
Background on SAT: normal forms, efficiently solvable subclasses, Tseitin encoding (Kroening and Strichman, Chapter 1)
Efficient SAT solving: the DPLL algorithm (Kroening and Strichman, Chapter 2.1, 2.2)
Lecture 18, 20 Mar 2014 (MKS) (Slides)
More on DPLL:
Lecture 19, 25 Mar 2014 (MKS) (Slides)
BDDs: Binary decision diagrams (see notes by Henrik Reif Andersen under Reading Material)
Lecture 20, 27 Mar 2014 (MKS) (Slides)
Equality logic and uninterpreted functions (Kroening and Strichman, Chapter 3)
Lecture 21, 1 Apr 2014 (MKS) (Slides)
Decision procedures for equality logic and uninterpreted functions (Kroening and Strichman, Chapter 4)
Lecture 22, 7 Apr 2014 (MM)
Linear arithmetic constraints
Lecture 23, 8 Apr 2014 (MM)
Linear arithmetic constraints
Lecture 24, 11 Apr 2014 (MKS) (Slides)
Decision procedures for equality logic and uninterpreted functions (Kroening and Strichman, Chapter 4; papers by Bryant and Velev, Meir and Strichman, and Rozanov and Strichman under Reading Material),)
Lecture 25, 15 Apr 2014 (MKS) (Slides)
Propositional encoding of decidable first order theories (Kroening and Strichman, Chapter 11)
Lecture 26, 17 Apr 2014 (MKS) (Slides)
Propositional encoding of decidable first order theories (Kroening and Strichman, Chapter 11)