On Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time

2021/10/07 by Guilloud, Simon, Kunčak, Viktor · 2 citations
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2110.03315

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.

Cited by

• LISA -- A Modern Proof System
• Orthologic Type Systems

Related

• BPA Bisimilarity is EXPTIME-hard
• Characterizing contrasimilarity through games, modal logic, and complexity
• The Bisimulation Problem for equational graphs of finite out-degree
• A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
• Simple grammar bisimilarity, with an application to session type equivalence