In this paper we discuss the new version of PITP, a proce- dure to decide propositional intuitionistic logic, which turns out at the moment to be the best propositional prover on ILTP. The changes in the strategy and implementation make the new version of PITP faster and capable of deciding more formulas than the previous one. We give a short account both of the old optimizations and the changes in the strategy with respect to the previous version. We use ILTP library and random generated formulas to compare the implementation described in this paper to the other provers (including our old version of PITP).
Avellone, A., Fiorino, G., Moscato, U. (2007). Improvements to the tableau prover PITP. In Proceedings of the 16th Conference Tableaux 2007 (pp.233-237). Berlin : Springer-Verlag.
Improvements to the tableau prover PITP
AVELLONE, ALESSANDRO;FIORINO, GUIDO GIUSEPPE;MOSCATO, UGO EMANUELE
2007
Abstract
In this paper we discuss the new version of PITP, a proce- dure to decide propositional intuitionistic logic, which turns out at the moment to be the best propositional prover on ILTP. The changes in the strategy and implementation make the new version of PITP faster and capable of deciding more formulas than the previous one. We give a short account both of the old optimizations and the changes in the strategy with respect to the previous version. We use ILTP library and random generated formulas to compare the implementation described in this paper to the other provers (including our old version of PITP).
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
