Nilpotence, bisimulation and the Unification Workbench

Equational unification is an important computational problem in automated deduction systems. Incorporating equational theories in unification algorithms has been guided by the properties of the functions that we often encounter in mathematical axioms. Nilpotent functions satisfy the axiom f(x,x) = 0. We study equational unification problems of nilpotence-related equational theories. Elementary unification modulo associativity, commutativity and nilpotence is shown to be NP-complete. If 0 is a unit of the nilpotent function then the equational theory is called ACUN. Elementary ACUN-unification can be solved in polynomial time. When a homomorphism is added, the equational theory becomes ACUNh. Elementary ACUNh-unification is still solvable in polynomial time. We extend ACUNh-unification to infinite terms and show that it remains in P. A subclass of set constraints is identified, which can be solved in polynomial time using the ACUNh-unification algorithm over infinite terms. The ground solvability of elementary ACUN-disunification is shown to be NP-complete. An interesting fact is that the relationship between the number of free constants and the numbers of disequations affects the complexity of solvability of disunification problems.; We study compatibility checking problems in process algebras using equational unification techniques. Unification in the bisimulation algebra is shown to be NP-complete. A subclass which contains only deterministic process expressions can be solved in polynomial time. Unification in the trace algebra is solvable in exponential time using tree automata. When only one action symbol is allowed, the unification problem in the trace algebra can be solved in polynomial time by reducing it to Horn clauses satisfiability.; Finally, we study efficient implementations of equational unification algorithms. We create an equational unification library and a graphic user interface. These are integrated into a software system called the Unification Workbench, which provides an experimental working environment for the study of equational unification.