Polynomial-time Equational Theory for Lattices with Unary Operators

期刊论文
出版模式：

开放获取
发表日期：

2025年6月21日

查看全文

C.J. Van Alten

摘要

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.