This repo contains an implementation of an algorithm able to solve the word problem for Orthocomplemented Bisemilattices. The original algorithm can be found in this paper: https://arxiv.org/abs/2110.03315 which has been published in TACAS 2022.

An Orthocomplemented Bisemillatice is a generalization of Boolean Algebra where distributivity doesn't hold. Hence, this algorithm provides a conservative approximation to the propositional equivalence problem.