UNIF 2013: Papers with AbstractsPapers 

Abstract. Automated reasoning modulo an equational theory E is a fundamental technique in many applications. In this talk, we would present a narrowingbased equational unification algorithm for theories satisfying the finite variant property. We also talk about equational generalization, also called antiunification  Abstract. The antiunification problem of two terms t<sub>1</sub> and t<sub>2</sub> is concerned with finding a term t which generalizes both t<sub>1</sub> and t<sub>2</sub>. That is, the input terms should be substitution instances of the generalization term. Interesting generalizations are the least general ones. The purpose of antiunification algorithms is to compute such least general generalizations.
Research on antiunification has been initiated more than four decades ago, with the pioneering works by Gordon~D.~Plotkin and John~C.~Reynolds. Since then, a number of algorithms and their modifications have been developed, addressing the problem in firstorder or higherorder languages, for syntactic or equational theories, over ranked or unranked alphabets, with or without sorts/types, etc. Antiunification has found applications in machine learning, inductive logic programming, casebased reasoning, analogy making, symbolic mathematical computing, software maintenance, program analysis, synthesis, transformation, and verification. Some of these algorithms and applications will be reviewed in the talk. We will also consider recent developments in unranked and higherorder generalization computation.  Abstract. We present an efficient encoding of ordersorted modular ACU terms into colored directed graphs. Then, by computing the automorphism groups of the encoded graphs, we are able to extract ACU structural symmetries both inside a term and across a set of terms. Finally, we show how the computed symmetries can be applied to the optimization of the equational generalization algorithms for modular ACU theories.  Abstract. Unification in Description Logics (DLs) has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the DL EL, which is used to define several large biomedical ontologies, unification is NPcomplete. However, the unification algorithms for EL developed until recently could not deal with ontologies containing general concept inclusions (GCIs). In a series of recent papers we have made some progress towards addressing this problem, but the ontologies the developed unification algorithms can deal with need to satisfy a certain cycle restriction. In the present paper, we follow a different approach. Instead of restricting the input ontologies, we generalize the notion of unifiers to socalled hybrid unifiers. Whereas classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are cyclic TBoxes, which are interpreted together with the ontology of the input using a hybrid semantics that combines fixpoint and declarative semantics. We show that hybrid unification in EL is NPcomplete  Abstract. In this work we study antiunification for unranked terms and hedges, permitting context and hedge variables. Hedges are sequences of unranked terms. The antiunification problem of two hedges s and q is concerned with finding their generalization, a hedge g such that both s and q are instances of g under some substitutions. Context variables are used to abstract vertical differences in the input hedges, and hedge variables are used to abstract horizontal differences. A rule based system in Huet's style will be presented, which computes a set of generalizations of input hedges and records all the differences. The computed generalizations are least general among a certain class of generalizations.  Abstract. Our main aim in this paper is to investigate an equational theory consisting of a number of identities or equivalences in Linear Temporal Logic (LTL) with the “until” operator U, but without the “nexttime” operator. We investigate unification problems modulo this theory. Two variants of unification are also studied, namely asymmetric unification and disunification. Our main focus is on algorithmic complexity.  Abstract. A critical question in unification theory is how to obtain a unification algorithm for the combination of nondisjoint equational theories when there exists unification algorithms for the constituent theories. The problem is known to be difficult and can easily be seen to be undecidable in the general case. Therefore, previous work has focused on identifying specific conditions and methods in which the problem is decidable. We continue the investigation in this paper, building on previous combination results and our own work. We are able to develop a novel approach to the nondisjoint combination problem. The approach is based on a new set of restrictions and combination method such that if the restrictions are satisfied the method produces an algorithm for the unification problem in the union of nondisjoint equational theories.  Abstract. We introduce a firstorder model of imperative sequential programs and set up formally the unification problem in this model: given a pair of programs π<sub>1</sub> and π<sub>2</sub> find a pair of substitutions (θ<sub>1</sub>,θ<sub>2</sub>) such that the instances π<sub>1</sub>θ<sub>1</sub> and π<sub>2</sub>θ<sub>2</sub> of these programs are equivalent, i.e. compute the same function. Since functional equivalence of programs is undecidable, we choose its decidable approximation  a strong equivalence,  which is wellknown in theory of program schemata. Our main result is a polynomial time unification algorithm for sequential programs w.r.t. strong equivalence of programs. 

