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

Willem Conradie, Valntin Goranko, Peter Jipsen

The non-deterministic algorithmic procedure PEARL (an acronym for `Propositional variables Elimination Algorithm for Relevance Logic') has been recently developed for computing fir…