The unification problem and several variants are presented. Various algorithms and data
structures are discussed. Research on unification arising in several areas of computer …

Most knowledge based systems in artificial intelligence (AI), with a commitment to asymbolic
representation, support one basic operation:“matching of descriptions”. This operation …

Publisher Summary This chapter focuses on rewrite systems, which are directed equations
used to compute by repeatedly replacing sub-terms of a given formula with equal terms until …

Roughly speaking, an equational problem is a first order formula whose only
predicatesymbol is=. We propose some rules for the transformation of equational problems …

We investigate the combination of propositional SAT checkers with domain-specific theorem
provers as a foundation for bounded model checking over infinite domains. Given a program …

This paper is concerned with E-unification in arbitrary equational theories. We extend the
method of transformations on systems of terms, developed by Martelli-Montanari for …

The unification problem in a disjoint combination of equational theories, E 1+...+ E n, is
reduced to a combination of two kinds of problems in the E j's: the pure unification, problem …

In this part we develop the framework for an order-sorted logic with equality, its syntax,
semantics and its computational aspects. The intention is that the first part provides …

Completion modulo a congruence is a method for constructing a presentation of an
equational theory as a rewrite system that defines unique normal forms with respect to the …

Solving equations in the free algebra T (F, X)(ie, unification) uses the two rules: ƒ (s)= ƒ (t)→
s= t (decomposition) and s [x]= x→⊥(occur-check). These two rules are not correct in …