Class Location/Time: SC1131 TR 11am - 12:15pm
Office Hours: SC 2108 TR 12:15pm - 1:15pm
Teaching Assistants: Stephen Skeirik (skeirik2) and Everett Hildenbrandt (hildenb2)
An Efficient Unification Algorithm - Martelli Montanari
This is a classical paper on syntactic unification (solving equations in term algebras). It specifies the algorithm by very simple inference rules rules and gives a simple proof of correctness. It also discusses well computational complexity issues.
Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification - Jouannaud Kirchner
This is an excellent survey paper about unification modulo an equational theory (Σ, E), and also about various extensions such as order-sorted unification, combination of algorithms, and even narrowing. One key value is the adoption throughout of the Martelli-Montanari viewpoint: each algorithm is specified in a declarative way by a set of inference rules (i.e. rewrite rules). Although we will not go into the details of each unification algorithm (there are many), I strongly recommend each student to do ate least a general reading of this paper to get the "lay of the land" about unification.
Canonical Forms and Unification - Hullot
This paper is one of the earliest and most cited ones about narrowing and about narrowing-based unification SEMI-algorithm for confluent and terminating equations by a then graduate student (you can also do stuff like that!) who was visiting SRI with his advisor (Gerard Huet) in my early times there. Some parts of the paper are unnecessary for the course. For example, previously basic narrowing was the best method to get narrowing to terminate (so it becomes an algorithm and satisfiability of QF+(Σ)-formulas in (Σ, TΣ(X)) is decidable), but basic narrowing terminates strictly less often than folding variant narrowing, which we will see later; so it is only of historical interest to look at the details of the basic narrowing strategy.
Strict Coherence of Rewriting Modulo Axioms - Meseguer
To obtain unification algorithms for theories whose equations are confluent MODULO axioms B, we need to understand two rewrite relations: →R/B and →R, B which can "simulate" efficiently →R/B. This has been a quite esoteric area with complicated and strange conditions and behaviors. This paper gives a much simpler notion of coherence assuming linear and regular axioms B. This will make the treatment of narrowing modulo B and of (E ∪ B)-unification easier. CS 476 lectures 4 and 5 are useful background for this paper. For the moment, you need only read Sections 1 and 2.
Folding Variant Narrowing and Optimal Variant Termination - Escobar Sasse Meseguer
This paper contains the best results known up to now about how to get efficient narrowing modulo B unification algorithms. Some parts are not necessary for the course, and some of it is dated; but it is still the main reference available. In the lectures I will provide a simpler explanation of everything. Still, I would suggest taking a first look at the paper to get a high-level impression without getting bogged down in technical details. The coming lectures will make all this clearer.
Dr. Meseguer's Notes on →R/B and →R, B
These notes describe the relationship between the relations →R/B and →R, B, e.g. when properites such as confluence and termination are preserved. Proofs are included. Some initial lemmas on irreducibility are also presented. These notes complement the Strict Coherence of Rewriting Module Axioms paper.
Dr. Meseguer's Notes on Narrowing
These notes define what narrowing is, show how it corresponds to the rewrite relation →R, B, and show how it can be used to obtain a unification algorithm.
Dr. Meseguer's Notes on Variant Narrowing
These notes define variants and variant narrowing and show how narrowing can be used to generate a complete set of variants.
The Finite Variant Property: How to Get Ride of Some Algebraic Properties
The original paper introduing the notion of variants and the finite variant property.
Variants of Variants and the Finite Variant Property
This paper explores different notions of variant proposed in the literature and shows how they relate to one another---including notions of variants as only terms, as only substitutions, and as pairs of a term and a substitution.
Dr. Meseguer's Notes on Folding Variant Narrowing
These notes define the boundness property, show it is equivalent to the FVP, and also define folding variant narrowing, show its completeness, and finally show how it can be used as a semi-algorithm to determine when a theory satisfies the FVP.
Dr. Meseguer's Notes on Variant Unfication
These notes describe and prove correct a unification algorithm based on folding variant narrowing.
Variant Satisfiability in Initial Algebras
As shown in Lecture 9, variant unification provides a theory-generic decision procedure for checking the satisfiability of a POSITIVE QF formula in the initial algebra TΣ/E ∪ B of any theory having an FVP decomposition and a finitary B-unification algorithm. The class of FVP theories is infinite and contains many theories of interest. This raises the following intriguing question: could we somehow EXTEND such a theory-generic decision procedure to a similar theory-generic decision procedure for satisfiability of ANY QF formula in the initial algebra TΣ/E ∪ B under similar, but somewhat stronger, assumptions on (Σ, E ∪ B)? The answer is YES!, and is contained in this paper, which will be discussed in a few lectures, starting with Lecture 10.
Metalevel Algorithms for Variant Satisfiability
These notes provide additional detail regarding the algorithms needed for variant satisfiability, including how to generate constructor variants and unifiers and how to check OS-compactness conditions.
A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm
Huet's paper on the correctness of KB completion algorithm is a classic. By computing critical pairs and orienting equations from left to right using a simplification order on terms one can, if successful, end up with a confluent and terminating set of equations equivalent to the original one given as input to the Knuth-Bendix algorithm. We are interested in the ground case of this algorithm to derive a correct-by-construction congruence closure algorithm.
Proof Lengths for Equational Completion
Plaisted and Sattler-Klein's ground KB-completion algorithm adds a few simplifications/strategies and some data structure assumptions to the gound version of Huet's KB-completion algorithm to derive an O(n^2) conguence closure algorithm.
Dr. Meseguer's Notes on Knuth-Bendix Completion
A review of the results of Huet and Plaisted & company plus proofs that decidability in the free models of empty theories is decidable.
Any Ground Associative-Commutative Theory Has a Finite Canonical System The paper by Narendran and Rusinowitz proves that a form of ground Knuth-Bendix completion modulo AC always terminates with a convergent set of ground rewrite rules equivalent to the original ground equations.
The paper by Barchmair et al. places "congruence closure" within an abstract, axiomatic setting as a set of inference rules. Basically, congruence closure is ground KB completion with the extra option of adding new constants besides those coming variables turned into constants; this can increase performance and decrease complexity from O(n^2) to O(n logn). What is nice about this paper is that:
different well-known algorithms are recovered as special cases based on different strategies to apply the inference rules;
they give also an AC congruence closure for the AC case.
Order-sorted Rewriting and Congruence Closure
The paper on order-sorted congruence closure proves a simple, yet surprising result: to do order-sorted congruence closure or order-sorted AC congruence closure you "don't have to do anything," that is, treating everything as unsorted yields correct decision procedures in both cases.
The paper by Rubio defines in detail the AC-RPO order, and proves that it defines a total order on AC congruence classes of ground terms. This order (or some similar order, but this is the best and simplest) is crucial to get AC congruence closure to work.
Reasoning About Recursively Defined Data Structures
This paper by Derek Oppen gave a general notion of (non-cyclic) recursive data structures, with lists a la LISP is a paradigmatic example and prove decidable QF satisfiability of such structures. Oppen used an unsorted typing, which of course makes his theory, while seminal, messy and unsatisfactory.
Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation, and Coercion Problems
This paper by Meseguer and Goguen gave a completely general solution to the problem of how to define selector functions that decompose into parts data elements built by free constructors for any recursive data structure. Although this paper was published a long time ago, the darkness of ignorance hangs like a plague over the topic of recursive data structures, which remains in the exact same conceptual mess as it was before this paper was published.
Combining Decision Procedures for Theories in Sorted Logics
The Tinelli-Zarba paper is the long version of a JELIA 2004, Springer LNAI 3229 paper. It is an important paper in at least two ways: (1) it provided foundations for many-sorted and order-sorted Nelson-Oppen combinations for the first time; and (2) it argued, convincingly, that the NO combination problem becomes both much easier to meet its conditions and more efficient by supporting sorts.
The Manna-Zarba paper is a very well-written survey of combination methods. It covers not only Nelson-Oppen and efficient inference systems for it, but gives also an up-to-date (as of 2003) survey of the state of the art on the alternative combination method by Shostak, which is more restrictive but has some advantages. For lack of time we will not be able to cover the Shostak method in CS 576, but this survey is a good introduction/explanation of it. Shostak's method lacked an actual proof of correctness for a long time, even though tools used it willy-nilly.
Complexity, Convexity, and Combination of Theories
This seminal paper by Oppen proposed the notion of convex theory and show how it can eliminate non-determinism from the NO procedure.
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing
Appendix A.3 of the Tinelli paper proves that every Horn Theory is convex. This appendix can be read with very little need to read the rest of the, also very nice, paper.
The paper by Nieuwenhuis, Oliveras and Tinelli is the standard reference on the DPLL(T) procedure, where, given a theory T with decidable QF satisfiability, instead of putting a QF formula ϕ in DNF and trying to check if some conjunction in it is T-satisfaible, a DPLL-based SAT solver works on the Boolean struncture of ϕ and extracts a conjunction that is then shown T-satisfiable in a more efficient manner.
Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
The Krstic-Goel paper generalizes DPLL(T) to DPLL(T1, …, Tn), where the T1, …, Tn are theories combined in the Nelson-Oppen manner. In this way, the power of SAT solvers is exploited for SMT solving not just for a single theory, but also for theory combinations.
Decision Procedures: An Algorithmic Point of View (Book)
This book by Strichman and Koening complements that of Bradley and Manna. It has a particularly good treatment of linear arithmetic. The two lectures on that topic will cover Sections 5.2 and 5.3 of the book, showing how linear arithmetic on the rationals and Presburger arithmetic on the integers can both be seen as instances of a general simplex-based algorithm. Other alternatives are also discussed in Chapter 5, but will not be covered in the two lectures.
A Logical Reconstruction of Reachability
The paper by Rybina and Voronkov is a good example of how SMT solving can be applied to symbolic model checking; specifically to its simplest version as symbolic reachability analysis used in the verification of invariants.
There is, of course, a vast literature on SMT-based symbolic model checking: this is just a sample as an "appetizer".
Superposition Modulo Linear Arithmetic SUP(LA)
The paper by Althaus et al. is a concrete example of how to answer the following general question:
How can general-purpose theorem proving and SMT solving be combined in a rigorous, systematic way?
General-purpose theorem proving can reason in ANY theory in a given logic. For example, the SPASS superposition-based first-order theorem prover, which is extended in this paper to handle linear arithmetic by SMT solving, can handle any universal first-order theory with equality. The weakness, however, is that its general methods cannot exploit the fact that a SUBTHEORY of the given theory is decidable; in this case the decidable subtheory chosen is linear arithmetic, but many other theories could have been chosen. What is perhaps most interesting is not the theory chosen, but the METHOD used: developing an inference system that extends the standard one for superposition to make it aware of solvable formulas in a subtheory.
Again, this is just a sample, an "appetizer." There is indeed a vast literature on adding decision procedures to theorem provers, and many successful theorem provers do support such decision procedures.