Algorithmic Correspondence for Relevance Logics, Bunched Implication Logics, and Relation Algebras via an Implementation of the Algorithm PEARL

The non-deterministic algorithmic procedure PEARL (acronym for 'Propositional variables Elimination Algorithm for Relevance Logic') has been recently developed for computing first-order equivalents of formulas of the language of relevance logics L-R in terms of the standard Routley-Meyer relational semantics. It succeeds on a large class of axioms of relevance logics, including all so called inductive formulas. In the present work we re-interpret PEARL from an algebraic perspective, with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras, and report on its recent Python implementation. We also show that all formulae on which PEARL succeeds are canonical, i.e., preserved under canonical extensions of relevant algebras. This generalizes the "canonicity via correspondence" result in [37]. We also indicate that with minor modifications PEARL can also be applied to bunched implication algebras and relation algebras.