View: session overviewtalk overviewside by side with other conferences
09:00  Handling substitutions via duality ABSTRACT. Many interesting problems concerning intuitionistic and intermediate propositional logics are related to properties of substitutions: among them, besides unification, we have rule admissibility, characterization of projective formulae, definability of maximum and minimum fixpoints, finite periodicity theorems, etc. Since all these questions can be stated in purely categorytheoretic terms, they are all sensible to an approach via duality techniques. The available duality for finitely presented Heyting algebras involves both sheaves (giving the appropriate geometric framework) and bounded bisimulations (handling the combinatorics of definability aspects): we show how to use such duality to attack and solve the above problems in a uniform way. [Recent and new results come from joint and ongoing work with Luigi Santocanale] 
10:00  SPEAKER: Joerg Siekmann ABSTRACT. At this time we only submit the abstract, which I uploaded under paper 
11:00  SPEAKER: Andrew M. Marshall ABSTRACT. We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In this note we extend this to consider a subterm convergent equational term rewrite system defined modulo an equational theory, like Commutativity or AssociativityCommutativity. We show that for certain classes of such equational theories, namely the shallow classes, the two knowledge problems remain decidable. 
11:30  SPEAKER: Ajay Kumar Eeralla ABSTRACT. We consider the problem of unification modulo an equational theory ACh, which consists of a function h which is homomorphic over an associativecommutative operator +. Unification modulo ACh is undecidable, so we define a bounded ACh unification problem. In this bounded version of ACh unification we essentially bound the number of times h can be recursively applied to a term, and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving bounded ACh unification, and we prove that the rules are sound, complete and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis. 
12:00  ABSTRACT. Topological logics are formalisms for reasoning about topological relations between regions. In this paper, we introduce a new inference problem for topological logics, the unifiability problem, which extends the validity problem by allowing one to replace variables by terms before testing for validity. Our main result is that, within the context of the mereotopology of all regular closed polygons of the real plane, unifiable formulas always have finite complete sets of unifiers. 
14:00  Compressed Term Unification: Results, uses, open problems, and hopes ABSTRACT. Already in the classic firstorder unification problem, the choice of a suitable formalism for term representation has a significant impact in computational efficiency. One can find other instances of this situation in some variants of secondorder unification, where representing partial solutions efficiently leads to better algorithms. 
15:00  SPEAKER: Pavlos Marantidis ABSTRACT. It is wellknown that the unification problem for a binary associativecommutativeidempotent function symbol with a unit (ACUIunification) is polynomial for unification with constants and in NP for general unification. We show that the same is true if we add a finite set of ground identities. 
16:00  SPEAKER: Cleo Pau ABSTRACT. Proximity relations are reflexive and symmetric fuzzy binary relations. They generalize similarity relations (similarity, in itself, is a generalization of equivalence in fuzzy setting) and have been introduced to deal with certain limitations of latter, related to incorrect representation of fuzzy information in some cases. Following [1], we consider signatures where some function symbols are allowed to be in a proximity relation with each other. In our opinion, such a representation is more adequate than similarity to deal with possible mismatches between the names of symbols. Our terms are firstorder terms, and the proximity relation is extended to them. In [1], a unification algorithm has been introduced for such terms. The problem we deal in this paper is a dual one: We are looking for generalizations, which, roughly, means that for two terms t1 and t2 we want to find a term r such that there exist substitution instances of r which are 'close enough to' (i.e., are in the given proximity relation with) t1 and t2. Interestingly, the problem of computing a minimal complete set of generalizations with respect to a given proximity relation requires computing all possible maximal vertexclique partitions in an undirected graph. We develop an algorithm for the all maximal clique partition problem, which is optimal in the sense that, first, it computes each maximal clique partition only once and, second, avoids generating and discarding false answers. Based on this method, we show that proximitybased antiunification has the finitary type and develop a terminating, sound, and complete algorithm for computing a minimal complete set of generalizations. [1] P. JuliánIranzo and C. RubioManzano. Proximitybased unification theory. Fuzzy Sets and Systems 262 (2015) 21–43. 
16:30  SPEAKER: David Cerna ABSTRACT. In “Generalisation de termes en theorie equationnelle. Cas associatifcommut atif”, a pair of terms was presented over the language { f (·, ·), g(·, ·), a, b}, where f and g are interpreted over an idempotent equational theory, i.e. g(x, x) = x and f (x, x) = x, resulting in an infinite set of generalizations. While this result provides an answer to the complexity of the idempotent generalization problem for arbitrarily idempotent equational theories (theories with two or more idempotent functions) the complexity of generalization for equational theories with a single idempotent function symbols was left unsolved. We show that the two idempotent function symbols example can be encoded using a single idempotent function and two uninterpreted constants thus proving that idempotent generalization, even with a single idempotent function symbol, can result in an infinite set of generalizations. Based on this result we discuss approaches to the handling generalization within idempotent equational theories. 
17:00  SPEAKER: Yunus David Kerem Kutz ABSTRACT. We consider rewriting, critical pairs and confluence tests on rewrite rules using nominal notation. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. The progress is that we permit atom variables in the notation and in the unification algorithm, which generalizes previous approaches using usual nominal unification 
17:30  SPEAKER: Anders Schlichtkrull ABSTRACT. We present a new formalization in the Isabelle proof assistant of firstorder syntactic unification, including a proof of termination. Our formalization follows, almost down to the letter, the MLcode from Baader and Nipkow's book "Term Rewriting and All That" (1998). Correctness is implied by the formalization's similarity to Baader and Nipkow's MLcode, but we have yet to formalize the correctness of the unification algorithm. 
17:50  SPEAKER: Weixi Ma ABSTRACT. We present a nominal unification algorithm that runs in $O(n \times log(n) \times G(n))$ time, where $G$ is the functional inverse of Ackermann's function. Nominal unification generates a set of variable assignments if there exists one, that makes terms involving binding operations $\alpha$equivalent. We preserve names while using special representations of de Bruijn numbers to enable efficient name management. We use MartelliMontanari style multiequation reduction to generate these name management problems from arbitrary unification terms.

Discussions about UNIF 2018 issues and future of UNIF
This is a dinner in a restaurant to be defined different from the FLOC dinner at Balliot College.
Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (prebooking via FLoC registration system required; guests welcome).