UNIF 2012: Papers with Abstracts

Papers
Recent Advances in Unification for the EL Family Franz Baader, Stefan Borgwardt and Barbara Morawska Abstract. Unification in description logics (DLs) has been proposed as a means to detect redundancies in ontologies. The DL EL, even though quite inexpressive, can be used to formulate large medical ontologies like SNOMED CT. Previously, several unification algorithms for EL were developed that can only deal with acyclic terminologies. In this paper, we give an overview over our recent efforts to generalize these algorithms to allow for general concept inclusions, transitive roles, and role hierarchies. For our new algorithms to be complete, the ontology needs to satisfy a certain cycle restriction.
The use of types in designing unification algorithms: two case studies Serdar Erbatur, Santiago Escobar and Paliath Narendran Abstract. We discuss the use of type systems in a non-strict sense when designing unification algorithms. We first give a new (rule-based) algorithm for an equational theory which represents a property of El-Gamal signature schemes and show how a type system can be used to prove termination of the algorithm. Lastly, we reproduce termination result for theory of partial exponentiation given earlier.
Some Notes on Basic Syntactic Mutation Kimberly Gero, Chris Bouchard and Paliath Narendran Abstract. Unification modulo convergent term rewrite systems is an important research area with many applications. In their seminal paper Lynch and Morawska gave three conditions on rewrite systems that guarantee that unifiability can be checked in polynomial time (P). We show that these conditions are tight, in the sense that relaxing any one of them will "upset the applecart," giving rise to unification problems that are not in P (unless P = NP). We also investigate a related decision problem: we show the undecidability of subterm-collapse for the restricted term rewriting systems that we are considering.
Bounded Higher-order Unification using Regular Terms Tomer Libal Abstract. We present an algorithm for the bounded unification of higher-order terms. The algorithm extends G. P. Huet's pre-unification algorithm with rules for the generation and folding of regular terms. The concise form of the algorithm allows the reuse of the pre-unification correctness proof. Furthermore, the regular terms can be restricted in order to decide the unifiability problem. Finally, the algorithm avoids re-computation of terms in a non-deterministic search which leads to a better performance in practice when compared to other bounded unification algorithms.