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.

An efficient relational deductive system for propositional non-classical logics

NICOLOSI ASMUNDO, MARIANNA
2006

Abstract

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.
Rasiowa-SIkorski proof systems; relational reasoning; non-classical logics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11769/31296
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact