Non-Ground Congruence Closure

TL;DR

This paper introduces a novel algorithm for directly computing non-ground congruence classes, which improves efficiency over traditional ground-based methods in handling non-ground equations.

Contribution

It presents a new sound and complete algorithm for non-ground congruence closure that outperforms classical ground algorithms in experiments.

Findings

Non-ground congruence classes can be computed more efficiently.

The proposed algorithm is sound and complete.

Experimental results show improved performance.

Abstract

Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence classes based on a given set of input equations, allowing ground equalities to be decided by membership. In many applications, these ground equations originate from grounding non-ground equations. We propose an algorithm that directly computes a non-ground representation of ground congruence classes for non-ground equations. Our approach is sound and complete with respect to the corresponding ground congruence classes. Experimental results demonstrate that computing non-ground congruence classes often outperforms the classical ground congruence closure algorithm in efficiency.