Madhavan Mukund

Theorem Proving

Jan-Apr, 2014

Course plan

• Resolution, Rewriting, Decision Procedures (to be elaborated)

• Instructors: Madhavan Mukund (MM), MK Srivas (MKS), SP Suresh (SPS)

• Guest lectures:, Deepak Kapur

Reading Material

• 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 Γ₀? 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.

  • Original paper: Supercomputing '91, IEEE/ACM (1991), 4-13.
  • Expanded version: Communications of ACM, 35(8) (1992) 102-114.

Assignments

• Assignment 1, 21 March 2014, due 7 April 2014

• Assignment 2, 15 April 2014, due 2 May 2014

Lecture summary

• 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

  • Vector addition systems. Completion procedure always terminates by Dickson's lemma.
  • Thue systems. Completion procedure may not terminate, Thue systems are Turing complete.
  • Group axioms. Use recursive path ordering and show that completion procedure terminates.

• Lecture 11, 13 Feb 2014 (Deepak Kapur)

  Clarification on lex ordering on strings

  Formal definition of superposition

  • Reduction as a special case of superposition

  Discovering a canonical rewrite system through completion

  • Fair derivations, ensure that all critical pairs are checked
  • Dealing with non-orientable critical pairs

  Semi-decision procedure for t = t',

  • Unfailing completion, attempt a reduction to normal form after each critical pair is completed

  Superposition calculus

  • Review first-order resolution: two rules, resolution and factoring.
  • Lifting order on terms to literals, clauses, proofs
  • New inference rules: positive/negative superposition, equality factoring
  • Some examples

• 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)

  • Termination of Ackermann rewrite system
  • Generalizations of lexicographic order to mixed and multiset order
  • Lexicographic path order is a simplification order

• 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:

  • Conflict driven learning and non-chronological backtracking (Slides, see the reference to GRASP under Reading Material),
  • VSIDS heuristic (see the reference to Chaff under Reading Material),

• 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

  • Generalized Simplex algorithm (Kroening and Strichman, Chapter 5.2)
  • Integer solutions: branch and bound (Kroening and Strichman, Chapter 5.3)
  • Fourier-Motzkin variable elimination (Kroening and Strichman, Chapter 5.4)

• Lecture 23, 8 Apr 2014 (MM)

  Linear arithmetic constraints

  • Integer solutions: Cutting planes (Gomory cuts) (Kroening and Strichman, Chapter 5.3.1)
  • Integer solutions: Omega test (Kroening and Strichman, Chapter 5.3)

• 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)