Polynomial-time Equational Theory for Lattices with Unary Operators
Clint J. van Alten · Order · 2025
Abstract The equational theory of the class of lattices with a pair of unary residuated operations is shown to be decidable in $$O(n^5)$$ O ( n 5 ) time. The same complexity holds in the bounded case. The equational theory of the class of lattices, as well as the class of bounded lattices, with a unary operator is shown to be decidable in $$O(n^3)$$ O ( n 3 ) time. Explicit algorithms are given for deciding the above equational theories. These algorithms use a dynamic programming approach and are based on a sequent calculus that extends Whitman’s sequent calculus for lattices.