Algorithm for determining equality of First-Order logic terms

Question

Can anyone guide me on how to implement an algorithm that can determine the equality of first-order logic terms. Here what's it look like.

• The terms consist only constant and function symbols. For example, $f(a, h(b, c))$.
• The premise can contain equality of any kinds of terms. For example, $\{f(a) = b, g(h) = x\}$

The algorithm would take 2 terms and list of equality premises and then derive a conclusion whether or not the terms are equal.

fn equals(first: Term, second: Term, equalities: List<(Term, Term)>) -> bool { ... }

For example, consider the term $f(a, b)$, $f(x, y)$, and equality premises of $\{x=a,y=b\}$, with these conditions, the term $f(a, b)$ should be equal with $f(x, y)$.

Currently, I only know about First-Order logic, Natural Deduction, and Unification. Is there an algorithm for this problem or which topics should I studied more?

Answer 1

There is no such algorithm. In particular, the problem of determining whether two elements of a finitely presented group are equal is undecidable. For documentation of that fact, see the Wikipedia page on the problem.