UNIF 2013: Papers with Abstracts

Abstract. Automated reasoning modulo an equational theory E is a fundamental technique in many applications. In this talk, we would present a narrowing-based equational unification algorithm for theories satisfying the finite variant property. We also talk about equational generalization, also called anti-unification

Abstract. The anti-unification problem of two terms t₁ and t₂ is concerned with finding a term t which generalizes both t₁ and t₂. That is, the input terms should be substitution instances of the generalization term. Interesting generalizations are the least general ones. The purpose of anti-unification algorithms is to compute such least general generalizations.

Research on anti-unification 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 first-order or higher-order languages, for syntactic or equational theories, over ranked or unranked alphabets, with or without sorts/types, etc. Anti-unification has found applications in machine learning, inductive logic programming, case-based 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 higher-order generalization computation.

Abstract. We present an efficient encoding of order-sorted 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 NP-complete. 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 so-called 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 NP-complete

Abstract. In this work we study anti-unification for unranked terms and hedges, permitting context and hedge variables.
Hedges are sequences of unranked terms.
The anti-unification 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 “next-time” 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 non-disjoint
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 non-disjoint
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 non-disjoint equational theories.

Abstract. We introduce a first-order model of imperative sequential programs and set up formally the unification problem in this model: given a pair of programs π₁ and π₂ find a pair of substitutions (θ₁,θ₂) such that the instances π₁θ₁ and π₂θ₂ 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 well-known in theory of program schemata. Our main result is a polynomial time unification algorithm for sequential programs w.r.t. strong equivalence of programs.