UNIF 2012:Papers with Abstracts

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.
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.
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.
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.