ABSTRACT. The unification problem in a modal or description logic is to determine whether given formulas have unifiers in that modal or description logic. When an instance of the unification problem has minimal complete sets of unifiers, it is either of type unitary, or finitary, or infinitary, depending on the cardinality of these sets. Otherwise, it is of type nullary. In this talk, we will survey the known results and we will present the recent advances about the unification types of modal and description logics.

ABSTRACT. We discuss unification within the simply-typed $\lambda$-calculus extended by a definition by cases operator (denoted by d) slightly differing from similar operators introduced by earlier investigations. Such operators may be thought of as restrictions of Hilbert's choice operator. We provide several non-trivial examples which illustrate the benefits of introducing such an operator.

ABSTRACT. Type checking and, to a larger extent, type and term inference in programming languages and proof assistants can be implemented by means of unification. In presence of dependent types, variations of higher-order unification are often used, such as higher-order pattern unification. In practice, there are often several mechanisms for abstraction and application, as well as other eliminators (such as projections from pairs) that have to be accounted for in the implementation of higher-order unification for a particular language. In this work, we study the possibility of representing various higher-order unification problems as a special case of E-unification for second-order algebra of terms. This allows us to present $\beta$-reduction rules for various application terms, and some other eliminators as equations, and reformulate higher-order unification problems as $E$-unification problems with second-order equations. We then present a procedure for deciding such problems, introducing second-order \emph{mutate} rule (inspired by one-sided paramodulation) and generic versions of \emph{imitate} and \emph{project} rules. We also provide a prototype Haskell implementation for syntax-generic higher-order unification based on these ideas in Haskell programming language.

ABSTRACT. This is a work-in-progress where we present a rule-based algorithm for nominal anti-unification of expressions in a higher-order language with lambda abstraction, functions symbols and recursive let. The algorithm is sound and weakly complete, but has high complexity.

ABSTRACT. This paper provides a generalized definition of the unification of Order-Sorted Feature (OSF) terms that considers a fuzzy subsumption relation between sort symbols rather than an ordinary (crisp) one. In this setting the unifier of two OSF terms is associated with a subsumption degree. We refer to the problem of unifying two OSF terms and computing the associated subsumption degree as fuzzy OSF term unification.

ABSTRACT. In this preliminary paper we report on the development of a new form of term rewrite system, the graph-embedded term rewrite system. These systems are inspired by the graph minor relation and are more flexible extensions of the well known homeomorphic embedded term rewrite systems. As a motivating application area for the new systems, we consider the symbolic analysis of security protocols. In this field, restricted term rewrite systems, such as subterm-convergent, have proven useful since many of the decision procedures are sound and complete for such systems. However, many of the same decision procedures still work for examples of systems which are "beyond subterm-convergent". Interestingly, the applicability of the decision procedure to these examples must typically be proven on an individual basis since they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that most of these systems are examples of graph-embedded term rewrite systems.

ABSTRACT. In a previous paper, we have investigated restricted unification in the Description Logic (DL) FL0. Here we extend this investigation to the DL FLbot, which extends FL0 with the bottom concept. We show that restricted unification in FLbot is decidable and provide some upper and lower bounds for the complexity. This is particularly interesting since the decidability status of unrestricted unification in FLbot appears to be still open. We also show an ExpTime lower bound for the unrestricted problem.