Guilloud, SimonKuncak, Viktor2022-03-072022-03-072022-03-07202210.1007/978-3-030-99527-0_11https://infoscience.epfl.ch/handle/20.500.14299/1860672110.03315We 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.Computer SciencePropositional LogicAlgorithmQuasilinearTerm Rewriting SystemLatticesOrthocomplemented Bisemilatticestext::conference output::conference proceedings::conference paper