Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

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
}