Polynomial-time Equational Theory for Lattices with Unary Operators

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)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>O</mml:mi> <mml:mo>(</mml:mo> <mml:msup> <mml:mi>n</mml:mi> <mml:mn>5</mml:mn> </mml:msup> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> 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)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>O</mml:mi> <mml:mo>(</mml:mo> <mml:msup> <mml:mi>n</mml:mi> <mml:mn>3</mml:mn> </mml:msup> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> 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.