# Asymmetric Unification and Disunification

## TL;DR

This paper compares two variants of equational unification, asymmetric unification and disunification, analyzing their computational complexities and showing they are incomparable in terms of solvability and complexity.

## Contribution

It provides a detailed complexity comparison of asymmetric unification and disunification, highlighting their differences and conditions affecting their computational difficulty.

## Key findings

- Asymmetric unification can be polynomial-time solvable in some theories.
- Disunification can be NP-hard even when asymmetric unification is polynomial.
- Complexity varies with the termination ordering of the rewriting system.

## Abstract

We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the right-hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory for the case with free constants. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in Polynomial time while the other is NP-hard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.