Intuitionistic Prover via S4 A Tableau Method Prover for Intutionistic Proposional Logic via S4 translation

, par Michel Lévy

It is well known that once a propositional formula A is translated into a modal formula B via Gödel translation, A is intuitionistically valid if and only if B is valid in S4. If A is intuitionistically valid, then the prover provides a proof that B is valid in S4. Si A is not intuitionistically valid, the prover provides a counter-model of B in S4.

Voir en ligne : Original web page