ABSTRACT. Unification and narrowing are a key ingredient not only to solve equations modulo an equational theory, but also to perform symbolic system analysis.  The key idea is that a concurrent system can be naturally specified as a rewrite theory (Sig,E,R), where (Sig,E) is an equational theory specifying the system's states as an algebraic data type, and R specifies the system's concurrent, and often non-deterministic, transitions.  One can perform such symbolic analysis by describing sets of states as (the instances of) terms with logical variables, and using narrowing modulo E to symbolically perform transitions.  Under reasonable conditions on the rewrite theory, this idea can be applied not only for complete reachability analysis, but also for temporal logic model checking. This approach is quite flexible but has some limitations.  Could it be possible to make symbolic system analysis  techniques more extensible and more widely applicable by simultaneously combining the powers of rewriting, narrowing, SMT solving and model checking? We give a progress report on current work aiming at such a unified symbolic approach.

ABSTRACT. Reasoning about data types is an important research area with many applications, such as formal program verification. Virtually all commonly used programming languages use lists or arrays and for certain Logic Programming languages, formal analysis via unification is a natural fit. Lists are also useful in the study of satisfiability modulo theories, which unification has strong connections to. In this paper, we investigate the unification problem modulo theories of lists. The different theories are obtained by considering observer functions of increasing complexity. These observer functions are right cons, reverse, and fold right (reduce.) In practice reduce is not a first-order function; we turn it into a first-order function by treating the binary function to be "folded" over the list as an uninterpreted function, i.e., as a constructor.

ABSTRACT. Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics (DLs) almost 20 years ago, motivated by applications in the Classic system. For the DL EL, it was shown in 2000 that the matching problem is NP-complete. It then took almost 10 years before this NP-completeness result could be extended from matching to unification in EL. The next big challenge was then to further extend these results from matching and unification without a TBox to matching and unification w.r.t. a general TBox, i.e., a finite set of general concept inclusions. For unification, we could show some partial results for general TBoxes that satisfy a certain restriction on cyclic dependencies between concepts, but the general case is still open. For matching, we were able to solve the general case: we can show that matching in EL w.r.t. general TBoxes is NP-complete. We also determine some tractable variants of the matching problem.

ABSTRACT. In the ordinary modal language, the normal modal logic Alt1 is the least normal logic containing the formula <>x->[]x. It can also be defined as the normal modal logic determined by the class of all deterministic frames. The unification problem in Alt1 is to determine, given a formula F(x1,...,xn), whether there exists formulas G1,...,Gn such that F(G1,...,Gn) is in Alt1. We demonstrate that the unification problem in Alt1 is decidable in polynomial space.

ABSTRACT. Asymmetric unification is a new paradigm for unification modulo theories that introduces irreducibility constraints on one side of a unification problem. It has important applications in symbolic cryptographic protocol analysis. However many facets of asymmetric unification that are of particular interest, including its behavior under combinations of disjoint theories, remain poorly understood. In this paper we give an overview of a new formulation of the method for unification in the combination of disjoint equational theories developed by Baader and Schulz that gives a new unification method for asymmetric unification in the combination of disjoint theories.

ABSTRACT. We present a new algorithm for the matching problem in the combination of non-disjoint equational theories. The method is an extension of our recent work on the hierarchical combination of unification algorithms.

ABSTRACT. Second-Order Unification is a problem that naturally arises when applying automated deduction techniques with variables denoting predicates. The problem is undecidable, but a considerable effort has been made in order to find decidable fragments, and understand the deep reasons of its complexity. Two variants of the problem, Bounded Second-Order Unification and Linear Second-Order Unification --where the use of bound variables in the instantiations is restricted--, have been extensively studied in the last two decades.  In this paper we summarize some decidability/undecidability/complexity results, trying to focus on those that could be more interesting for a wider audience, and involving less technical details.

ABSTRACT. Motivated by the study of admissible rules, a new hierarchy of ``exact'' unification types is introduced where a unifier is more general than another unifier if all identities unified by the first are unified by the second. A Ghilardi-style algebraic interpretation of this hierarchy is presented that uses exact algebras rather than projective algebras. Examples of equational classes distinguishing the two hierarchies are also provided.

ABSTRACT. SGGS (Semantically-Guided Goal-Sensitive theorem proving) is a clausal theorem-proving method, with a seemingly rare combination of properties: it is first order, DPLL-style model based, semantically guided, goal sensitive, and proof confluent. SGGS works with constrained clauses, and uses a sequence of constrained clauses to represent a tentative model of the given set of clauses. A basic building block in SGGS inferences is splitting, which partitions a clause into clauses that have the same set of ground instances. Splitting introduces constraints and their manipulation, which is the subject of this paper.

ABSTRACT. It is generally accepted that to unify a pair of substitutions $\theta_1$ and $\theta_2$ means to find out a pair of substitutions $\eta'$ and $\eta''$ such that the compositions $\theta_1\eta'$ and $\theta_2\eta''$ are the same. Actually, unification is the problem of solving linear equations of the form $\theta_1X=\theta_2Y$ in the semigroup of substitutions. But some other linear equations on substitutions may be also viewed as less common variants of unification problem. In this paper we introduce a two-sided unification as the process of bringing a given substitution $\theta_1$ to another given substitution $\theta_2$ from both sides by giving a solution to an equation $X\theta_1Y=\theta_2$. Two-sided unification finds some applications in software refactoring as a means for extracting instances of library subroutines in arbitrary pieces of program code. In this paper we study the complexity of two-sided unification and show that this problem is NP-complete by reducing to it the bounded tiling problem.

ABSTRACT. We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context.

ABSTRACT. In 1991 Miller described a subset of the higher-order unification problem for the Simply Typed Lambda Calculus which admits most general unifiers, called the pattern fragment. This subset has been extended to more complex type theories and it is still used as the basis of modern unification algorithms in applications like proof search and type inference. Our contribution is a new presentation of the original unification algorithm that focuses on the abstract properties of the operations involved, using category theory as a structuring principle. These properties characterize a class of languages for which the algorithm can be reused.

ABSTRACT. The unification algorithm is at the heart of a proof assistant like Coq. In particular, it is a key component in the refiner (the algorithm who has to fill implicit terms and missing type annotations), and the application of lemmas. Despite of being so important, however, the current unification algorithm of Coq is not properly documented, and implements certain heuristics that makes unification unpredictable and hard to understand.

In this work we discuss some of the problems with the current algorithm and present a new one, built from scratch, which aims at solving these issues. The new algorithm is properly documented, putting us on better grounds for a formally verified and optimized algorithm.