An efficient relational deductive system for propositional non-classical logics

We describe a relational framework that uniformly supports formalization and automated reasoning in various 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 a number of refinements.

• Type: Journal
• Year: 2006
• Where: JANCL
• Authors: Andrea Formisano, Marianna Nicolosi Asmundo
• Keywords: Classical Rasiowa-sikorski Proof, Compact Graph-based Representation, JANCL 2006, Propositional Modal Logics