This is a Java implementation of the equational anti-unification algorithm for nominal terms described in:

• Alexander Baumgartner and Daniele Nantes-Sobrinho, Nominal Anti-Unification Modulo Equational Theories, Preprint submitted to Journal of Logical and Algebraic Methods in Programming, 2025.

The algorithm solves the following problem:

GIVEN:	Two nominal terms-in-context (∇, s) and (∇, t).
FIND:	A nominal term-in-context (Γ, r) that is a least general E-generalization of (∇, s) and (∇, t).

Input Syntax

In the input 3 disjoint sets of symbols are used: function symbols, atoms and variables. Symbol names can be of arbitrary length.

• If the first letter of the symbol name is within a - e or A - E, then it is an atom.
• If the first letter of the symbol name is within u - z or U - Z, then it is a variables.
• Otherwise it's a function symbol. Function applications of arity zero f() may be written as just f.
• Associative function applications may be written in flattened form. I.e., f(a,b,c) may be used instead of writing f(f(a,b),c).
• The dot "." is used for abstraction.
• The sharp "#" is used for freshness constrains.

Anti-unification problem: (Use the semicolon to separate the equations of the system.) f(a,b) =^= f(b,a) Freshness context ∇: Extra atoms: Commutative symbols ℂ: Associative symbols 𝔸: Use branching heuristics:  Aligns arguments of commutative function applications. -1 = no limit Output format: Simple Verbose Progress Debug all   compact Output lines limit: -1 = no limit Compute Generalizations   Compute Linear Generalizations

Output