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.