UNIF on Wednesday, July 14th

09:00‑10:00 Invited Talk
Chair: Maribel Fernández and Laurent Vigneron
Location: AT LT3
09:00 Claude Kirchner (INRIA Bordeaux-Sud-Ouest, France)
Antipatterns: how to say what you don't want to match to
10:30‑12:30 Session 1
Chair: Maribel Fernández
Location: AT LT3
10:30 Sunil Kothari and James Caldwell
A Machine Checked Model of Idempotent MGU Axioms For a List of Equational Constraints

Machine checked proofs of type inference algorithms often axiomatize MGU behavior as a set of axioms. Idempotent MGUs for a list of equational constraints are needed to reason about the correctness of Wand's type reconstruction algorithm and our extension of it. To characterize the behavior of idempotent MGUs, we propose a set of seven axioms; four of which have been proven in our earlier paper, where we formally verify that the first order unification is a model for the axioms. This paper shows that the first order unification is a model for the remaining three idempotent MGU axioms. Our constraints are equalities between terms in a language of simple types and we model substitutions as finite maps from the Coq library {\it Coq.FSets.FMapInterface}. Coq's method of functional induction is the main proof technique used in proving the axioms.

11:00 Franz Baader and Barbara Morawska
SAT Encoding of Unification in EL

In previous work, we have shown that unification in the description logic EL is NP-complete. However, the algorithm used to establish the NP upper bound is a brutal "guess and then test" NP-algorithm. In this paper, we describe a new decision procedure for unification in EL that is based on a reduction to propositional satisfiability. This allows us to use a highly-efficient SAT solver in order to decide EL-unifiability. Our SAT-translation is inspired by Kapur and Narendran's translation of ACIU-unification problems into HornSAT, but it also generates non-Horn clauses.

11:30 Deepak Kapur, Andrew Marshall and Paliath Narendran
Unification modulo a partial theory of exponentiation

Modular exponentiation is a common mathematical operation in modern cryptography. This, along with modular multiplication at the base and exponent levels (to different moduli) plays an important role in a large number of key agreement protocols. In our earlier work [4, 5] we gave many decidability as well as undecidability results for multiple equational theories, involving various properties of modular exponentiation. Here, we consider a partial subtheory focussing only on exponentiation and multiplication operators. Two main results are proved. The first result is positive, namely, that the unification problem for the above theory (in which no additional property is assumed of the multiplication operators) is decidable. The second result is negative: if we assume that the two multiplication operators belong to two different abelian groups, then the unification problem becomes undecidable. This result is established using a construction patterned after those employed in [4, 6] by reducing Hilbert's 10th problem to the unification problem.

12:00 Conrad Rau and Manfred Schmidt-Schauß
Towards Correctness of Program Transformations Through Unification and Critical Pair Computation

Correctness of program transformations in extended lambda-calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, which results in so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting system. We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study of an application we describe a finitary and decidable unification algorithm for the combination of equational theories, contexts and many-sorted unification where equational theories are restricted have linear axioms, permits an occurs-check, and having a finitary unification algorithm only applied to sets of equations where every context variable occurs at most once and must have free argument-sorts.

14:00‑15:00 Invited Talk
Chair: Maribel Fernández and Christopher Lynch
Location: AT LT3
14:00 Christian Urban (Technical University Munich, Germany)
Nominal Unification - Hitting a Sweet Spot
15:30‑17:30 Session 2
Chair: Jordi Levy
Location: AT LT3
15:30 Christophe François Olivier Calvès
Nominal Theory as an Extension of First-Order Theory

Nominal techniques were introduced to represent in a simple and natural way systems that include binders. In this paper we present a morphism from nominal theory to first-order theory and use it to extend Paterson and Wegman's linear first-order unification algorithm, Tarjan's union-find algorithm and Martelli and Montanari's almost-linear first-order unification algorithm thus obtaining respectivly a quadratic nominal unification algorithm, an efficient nominal-aware union-find algorithm and an almost-quadratic nominal algorithm.

16:00 Sergiu Bursuc and Cristian Prisacariu
Unification and matching in separable theories

We study problems of unification and matching in equational theories based on semirings. These theories include Kleene algebra and its extensions with different forms of concurrency, constraint semirings, and synchronous actions algebra. Generally the unification problems are undecidable in this setting, but different undecidability proofs are required. On the other hand, the matching problems are decidable and a general pattern can be drawn. This pattern is developed into a matching algorithm, relying on a new way of combining non-disjoint theories, which we call stratification, and on a relaxation of the finite variant property, which we call separability. Consequently, we believe that our algorithm and the notions that we introduce have an importance i) beyond theories based on semirings; ii) for other problems related to unification and matching.

16:30 Zhiqiang Liu and Christopher Lynch
Efficient XOR Unification

We give efficient sets of inference rules for unification with uniterpreted function symbols modulo each of the following theories: XOR, XOR with homomorphism, abelian group, and abelian group with homomorphism.

17:00 Paliath Narendran, Andrew Marshall and Bibhu Mahapatra
On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity

We prove that the current algorithm presented in Tiden and Arnborg [9] is not polynomial time bounded as previously thought. A set of counter examples is developed that demonstrates that the present algorithm goes through exponentially many steps.