UNIF 2012 is the 26th event in a series of international meetings devoted to unification theory and its applications. The list of previous meetings can be found at UNIF web page.

The aim of UNIF 2012, as that of the previous meetings, is to bring together researchers interested in unification theory and related topics, to present recent (even unfinished) work, and discuss new ideas and trends in this and related fields. This includes scientific presentations, but also descriptions of applications and softwares using unification as a strong component.

This year’s UNIF is a satellite event of the IJCAR 2012 conference which is part of the Alan Turing Year 2012, and collocated with The Alan Turing Centenary Conference. UNIF 2012 will be held on July 1st, at the,University of Manchester, School of Computer Science, UK.

Registration is part of IJCAR 2012 registration.

Informal proceedings UNIF 2012

Invited speakers

  • Franz Baader

    Unification and Related Problems in Modal and Description Logics
    Abstract. Unification modulo equational theories was originally introduced in automated deduction and term rewriting, but has recently also found applications In
    modal logics and description logics. In this talk, we review problems and
    results for unification in description logics, and relate them to equational
    unification and unification in modal logics. Related problems, like disunification,
    rigid E-unification, and admissibility of inference will also be considered.

  • Emil Jeřábek
    Rules with parameters in modal logic
    Abstract. While admissible rules and unification are fairly well understood in
    transitive modal logics, rules with parameters have so far received
    less attention. We know from the work of Rybakov that admissibility
    of rules with parameters is decidable and complete sets of unifiers
    are computable for basic transitive modal logics. In this talk, we
    will discuss other aspects of rules with parameters in basic
    transitive logics, such as the computational complexity of
    admissibility and unification, and bases of admissible rules.

Topics of Interest

A non-exhaustive list of topics of interest:

  • Unification algorithms, calculi and implementations
  • Equational unification and unification modulo theories: algorithms and calculi
  • 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
  • Applications of unification

Submission Details

Submissions should not exceed 5 pages in LNCS style. Papers should be submitted in PDF- or PS-format through EasyChair.

Informal proceedings with the accepted papers will be available in electronic form on UNIF web page. Based on the number and quality of submissions we will consider organising formal proceedings of extended versions of papers in EPTCS.