paper ps
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.

### Citation

Simon Guilloud and Viktor Kunčak.
Equivalence checking for orthocomplemented bisemilattices in
log-linear time.
In *TACAS*, 2022.### BibTex Entry

@inproceedings{GuilloudKuncak22EquivalenceCheckingOrthocomplementedBisemilatticesLogLinearTime,
author = {Simon Guilloud and Viktor Kun\v{c}ak},
title = {Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time},
booktitle = {TACAS},
abstract = {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.},
year = 2022
}