Congruence Closure Modulo Permutation Equations

TL;DR

This paper introduces a polynomial-time framework for congruence closure modulo permutation equations, extending existing methods to handle specific interpreted function symbols and producing convergent rewrite systems.

Contribution

It extends the abstract congruence closure framework to permutation equations and certain interpreted functions, enabling polynomial-time decision procedures.

Findings

Framework handles permutation function symbols effectively

Constructs convergent rewrite systems for ground equations

Provides polynomial-time decision procedure for word problem

Abstract

We present a framework for constructing congruence closure modulo permutation equations, which extends the abstract congruence closure framework for handling permutation function symbols. Our framework also handles certain interpreted function symbols satisfying each of the following properties: idempotency (I), nilpotency (N), unit (U), I U U, or N U U. Moreover, it yields convergent rewrite systems corresponding to ground equations containing permutation function symbols. We show that congruence closure modulo a given finite set of permutation equations can be constructed in polynomial time using equational inference rules, allowing us to provide a polynomial time decision procedure for the word problem for a finite set of ground equations with a fixed set of permutation function symbols.