Welcome to UNIF 2018 in Oxford

UNIF 2018 will be the 32nd 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.

UNIF 2018 is affiliated with the Third International Conference on Formal Structures for Computation and Deduction FSCD 2018, part of the Federated Logic Conference 2018 () in Oxford.

Call for Papers

The International Workshop on Unification is a yearly forum for researchers in unification theory and related fields to meet old and new colleagues, to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for young researchers and scientists working in related areas to get an overview of the state of the art in unification theory. UNIF welcomes submissions describing research on all aspects of unification and its applications. Suggested topics include but are not limited to the following:

Unification algorithms, calculi and implementations Equational unification and unification modulo theories
Unification in modal, temporal and description logics Admissibility of Inference Rules
Narrowing Matching algorithms
Constraint solving Combination problems
Disunification Higher-Order Unification
Type checking and reconstruction Typed unification
Complexity issues Query answering
Implementation techniques Formalisation of unification
Applications of unification

Submission instructions

Following the tradition of UNIF, we call for submissions of abstracts (5 pages) in EasyChair style, to be submitted electronically as PDF files through the EasyChair submission site:

http://easychair.org/conferences/?conf=unif2018

Abstracts will be evaluated by the Programme Committee (if necessary with support from external reviewers) regarding their significance for the workshop. We will allow work presented/submitted in/to another conference.

Accepted abstracts will be presented at the workshop and included in the informal proceedings of the workshop, available in printed form at the workshop and in electronic form from the UNIF homepage.

Based on the number and quality of submissions we will decide whether to organise a special journal issue.

Important Dates

  • Submission of title and abstracts: Monday, April 9, 2018
  • Submission of full paper: Monday, April 16, 2018
  • Author notification: Tuesday, May 15, 2018
  • Camera-ready papers: Monday, May 28 25, 2018
  • UNIF 2018: Saturday, July 7, 2018
  • FSCD 2018: July 9-12, 2018
  • Main conference (FLoCS): July 6-19, 2018

Invited Speakers

Silvio Ghilardi (Università degli Studi di Milano)
"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 category-theoretic 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]

Adrià Gascón (The Alan Turing Institute / University of Warwick)
"Compressed Term Unification: Results, uses, open problems, and hopes"
Abstract: Already in the classic first-order 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 second-order unification, where representing partial solutions efficiently leads to better algorithms.
In this talk I will present some compression schemes for terms and discuss computational complexity results for variants of first and second-order unification on compressed terms. I'll show how these results build up on each other and discuss open problems in compressed term unification, as well as potential approaches to solutions.

Committees

PC Chairs

  • Mauricio Ayala-Rincón (Universidade de Brasília)
  • Philippe Balbiani (CNRS - Toulouse University)
    •

    Program Committee

  • Maria Alpuente (UP Valencia)
  • Franz Baader (TU Dresden)
  • Eduardo Bonelli (UN Quilmes)
  • Iliano Cervesato (Carnegie Mellon U)
  • Wojciech Dzik (U Silesia)
  • Santiago Escobar (UP Valencia)
  • Maribel Fernández (King's College London)
  • Çigdem Gencer (Istanbul Aydin U)
  • Rosalie Iemhoff (U Utrecht)
  • Emil Jeřábek (Czech Academy of Sciences)
  • Temur Kutsia (Johannes Kepler U Linz)
  • Jordi Levy (IIIA-CSIC)
  • Christopher Lynch (Clarkson U)
  • Catherine Meadows (US Naval Research Laboratory)
  • Paliath Narendran (U at Albany - State U of New York)
  • Christophe Ringeissen (Inria Nancy)
  • Manfred Schmidt-Schauß (Johann Wolfgang Goethe U Frankfurt)

    • UNIF Steering Committee

  • Barbara Morawska, Technische Universität Dresden
  • Konstantin Korovin, University of Manchester
  • Christophe Ringeissen, Inria Nancy
  • Temur Kutsia, RISC Johannes Kepler Universität Linz
  • Mateu Villaret, Universitat de Girona
  • Santiago Escobar, Universitat Politècnica de València
  • Silvio Ghilardi, Università degli Studi di Milano
  • Manfred Schmidt-Schauß, Goethe Universität Frankfurt am Main
    •

    Accepted Papers (UNIF 2018 Program at FLoC) (Informal proceedings)

  • Joerg Siekmann and Peter Szabo.
    Unification Based on Generalized Embedding
  • Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen.
    Knowledge Problems in Equational Extensions of Subterm Convergent Theories
  • Ajay Kumar Eeralla and Christopher Lynch.
    Bounded ACh Unification
  • Çigdem Gencer.
    About the Unification Type of Topological Logics over Euclidean Spaces
  • Franz Baader, Pavlos Marantidis and Antoine Mottet.
    ACUI Unification Modulo Ground Theories
  • Cleo Pau and Temur Kutsia.
    Proximity-Based Generalization
  • David Cerna and Temur Kutsia.
    Towards Generalization Methods for Purely Idempotent Equational Theories
  • Yunus David Kerem Kutz and Manfred Schmidt-Schauss.
    Rewriting with Generalized Nominal Unification
  • Kasper Fabæch Brandt, Anders Schlichtkrull and Jørgen Villadsen.
    Formalization of First-Order Syntactic Unification
  • Weixi Ma, Jeremy Siek, David Christiansen and Daniel Friedman.
    Efficiency of a Good but not Linear Nominal Unification Algorithm