An efficient relational deductive system for propositional non-classical logics

We describe a relational framework that uniformly supports formalization and automated reasoning in varied propositional modal logics. The proof system we propose is a relational variant of the classical Rasiowa-Sikorski proof system. We introduce a compact graph based representation of formulae and proofs supporting an efficient implementation of the basic inference engine, as well as of number of refinements. Completeness and soundness results are shown and a Prolog implementation is described.