# On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

arXiv: https://arxiv.org/abs/2110.03315 · HTML: https://mlsanity.com/paper/2110.03315/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Oct 2021.

## Built on by (most cited first, 1 of 1)

- [Orthologic for SAT Solving](https://mlsanity.com/paper/2605.16421/) (2026)

## Abstract (arXiv)

We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomorphism which we combine with a term rewriting system to decide equivalence of two terms. We prove that the rewriting system is terminating and confluent and hence the existence of a normal form, and that our algorithm is computing it. We also discuss applications and present an effective implementation in Scala.