Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)

TL;DR

The paper presents PEARL, an algorithm for translating relevance logic formulas into first-order logic, reinterprets it algebraically, reports on its Python implementation, and extends its applicability to related algebraic structures.

Contribution

It reinterprets PEARL algebraically, proves its success on canonical formulas, and extends its application to bunched implication and relation algebras.

Findings

PEARL successfully computes first-order equivalents for a broad class of relevance logic formulas.

All formulas on which PEARL succeeds are shown to be canonical.

PEARL can be adapted with minor modifications to bunched implication and relation algebras.

Abstract

The non-deterministic algorithmic procedure PEARL (an 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 RL 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 Urquhart's 1996 paper. We also indicate that, with minor modifications, PEARL can be applied to bunched implication algebras and relation algebras.