UNIF 2019 - 33rd International Workshop on Unification

June 24, 2019

UNIF 2019 will be the 33rd in a series of annual international workshops on unification. Previous editions have taken place mostly in Europe (Austria, Denmark, France, Germany, Ireland, Italy, Poland, UK), but also in the USA and Japan. For more details on previous UNIF workshops, please see the UNIF homepage.

Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense, encompassing also research in constraint solving, admissibility of inference rules, and applications such as type checking, query answering and cryptographic protocol analysis.

The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice.

Topics of interest to this forum include, but are not limited to:

  • Unification algorithms, calculi and implementations
  • Equational unification and unification modulo theories
  • Admissibility of Inference Rules
  • Unification in modal, temporal and description logics
  • Narrowing
  • Formalisation of unification
  • Matching Problems
  • Applications
  • Unification in Special Theories
  • Higher-Order Unification
  • Combination problems
  • Contraint Solving
  • Disunification
  • Complexity Issues
  • Type Checking and reconstruction

UNIF 2019 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. More information about UNIF can be found by clicking here.

UNIF 2019 will be a satellite workshop of Formal Structures for Computation and Deduction (FSCD'19) in Dortmund. Previous editions took place in Oxford/UK (2018 and 2017), Porto/ Portugal (2016), Warsaw/Poland (2015), etc.


UNIF 2019 Proceedings

Co-located with FSCD'19 .
Dortmund - Germany
June 24-29, 2019


UNIF 2019 Proceedings

UNIF 2019 Location Information

Seminar Room 1.055
Computer Science Faculty Building
TU Dortmund
Otto - Hahn Str. 12
44227 Dortmund



Catering: room 1.054

Check the Program !!

Confirmed Invited Speakers

Jörg Siekmann
(Saarland University/DFKI)

Narciso Martí Oliet
(Universidad Complutense Madrid)

Contact us


Call for Papers

Contributions should be written in English and submitted in the form of abstracts with a maximum of 5 pages including references in EasyChair style . The submission should be in the form of a PDF file uploaded to Easychair:


The workshop pre-proceedings, containing the reviewed extended abstracts, will be handed-out at workshop registration. At least one of the authors should register for the workshop. Presentations should be in English. According to the quality of proceedings, authors will be invited to submit an improved version of their paper for a special journal issue.

Important Dates

  • Title and Abstract: April 14, 2019 April 21, 2019
  • Paper Submission: April 21, 2019 April 28, 2019
  • Notification to authors:   May 31, 2019
  • Workshop date:   June 24, 2019

Invited Speakers

  • Jörg Siekmann - Saarland University/ DFKI
    Rethinking Unification Theory
    Abstract: Let us lean back for a minute and reflect on the motivation for our field. Apart from its theoretical interest, i.e. the structural relationships among and within equational theories, there is the practical motivation, most clearly expressed in Gordon Plotkin's seminal paper from 1972 [10]: we want to take certain troublesome axioms, like associativity or commutativity, out of the axiom set for an automated deduction system that may lead the system to go astray. Instead - so the proposal - they should be “built-in”.
    Now the past 30 years - the first workshop in Val D‘Ajol was in 1987 - have revealed an astonishing complexity even for those simple axioms - not so astonishing after all, for someone familiar with semigroup theory [3] and more generally the results about equational theories [7, 6].

    Full Abstract: Rethinking Unification Theory

  • Narciso Martí-Oliet - Universidad Complutense Madrid, Spain
    Maude strategies for narrowing
    (joint work with L. Aguirre, M. Palomino, and I. Pita)

    Abstract: Strategies allow modular separation between the rules that specify a system and the way that these rules are applied. They can be used both to implement and test different algorithms over a given specification or to drive the search of solutions to reachability problems reducing the state space. A strategy language for rewriting using Maude has been developed and implemented during the last years. The language controls when a basic step of rewriting is taken, by using sequences, tests, and other combinators. The next Maude release will include full support for this strategy language. The ongoing work that we present extends the use of this strategy language to narrowing, which is a more general method than rewriting and may have a much larger state space for a given problem, because whereas rewriting uses matching for solving reachability problems, narrowing uses unification. The application of a basic narrowing step is controlled in this case by means of a subset of the strategy combinators defined for rewriting. Narrowing strategies can turn an infinite state space into a finite one, as it has already been shown in an example using the prototype that we have developed. This prototype is a proof of concept to settle the basis of what can be achieved using strategies in a narrowing environment.


24 June 2019

Session 1   Chair: Daniele Nantes
  • 9:00 - 10:00 Invited Talk: Rethinking Unification Theory
           Jörg Siekmann
10:00 - 10:30 Coffee-Break

Session 2   Chair: Temur Kutsia
  • 10:30 Unification of Multisets with Multiple Labelled Multiset Variables
  •       Zan Naeem and Giselle Reis
  • 11:00 Formalising Nominal AC-Unification
  •       Mauricio Ayala-Rincón, Maribel Fernández and Gabriel Ferreira Silva
  • 11:30 Parameters for Associative and Commutative Matching
  •       Luis Bustamante, Ana Teresa Martins and Francicleber Ferreira
  • 12:00 On Forward-closed and Sequentially-closed String Rewriting Systems
  •       Yu Zhang, Paliath Narendran and Heli Patel
12:30 - 14:00 Lunch Break

Session 3   Chair: To be defined.
  • 14:00 Nominal Unification with Letrec and Environment-Variables
  •       Manfred Schmidt-Schauss and Yunus David Kerem Kutz
  • 14:30 On Asymmetric Unification for the Theory of XOR with a Homomorphism
  •       Christopher Lynch, Andrew M Marshall, Catherine Meadows, Paliath Narendran and Veena Ravishankar
  • 15:00 A Coq Formalization of Boolean Unification
  •       Daniel Dougherty
15:30 - 16:00 Coffee - Break

Session 4   Chair: Manfred Schmidt-Schauss
  • 16:00 - 17:00 Invited Talk: Maude strategies for narrowing
  •          Narciso Martí-Oliet
  • 17:00 Solving Proximity Constraints
  •       Temur Kutsia and Cleo Pau
  • 17:30 Asymmetric Unification and Disunification for the theory of Abelian groups with a homomorphism (AGh)
  •       Veena Ravishankar, Paliath Narendran and Kimberly Cornell


Program Commitee

Organising Commitee

  • FSCD Conference Chair: Jakob Rehof (TU Dortmund) - jakob.rehof(at)cs.tu-dortmund.de
  • FSCD Workshops Chair: Boris Düdder (TU Dortmund)- boris.d(at)di.ku.dk


See the FSCD 2019 Webpage


For more information please contact the chairs:
Daniele Nantes (dnantes(at)mat.unb.br)   -   PC co-chair
Serdar Erbatur (serdar.erbatur(at)ifi.lmu.de)   -   PC co-chair