The contribution of this paper consists in some techniques to bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and they are the backbone of a tableau based theorem prover (PITP) implemented in C++ language. PITP and some known theorem provers are compared by the formulas of ILTP v1.1 benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library
Avellone, A., Fiorino, G., Moscato, U. (2006). A tableau decision procedure for propositional intuitionistic logic. In Proceedings of the 6th International Workshop on the implementation of Logics (pp.64-79). Phnom Penh : CEUR.
A tableau decision procedure for propositional intuitionistic logic
AVELLONE, ALESSANDRO;FIORINO, GUIDO GIUSEPPE;MOSCATO, UGO EMANUELE
2006
Abstract
The contribution of this paper consists in some techniques to bound the proof search space in propositional intuitionistic logic. These techniques are justified by Kripke semantics and they are the backbone of a tableau based theorem prover (PITP) implemented in C++ language. PITP and some known theorem provers are compared by the formulas of ILTP v1.1 benchmark library. It turns out that PITP is, at the moment, the propositional prover that solves most formulas of the library
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
