On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

10/07/2021
by   Simon Guilloud, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset