Title
Improvements to the Tableau Prover PITP
Abstract
In this paper we discuss the new version of PITP, a procedure 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).
Year
DOI
Venue
2007
10.1007/978-3-540-73099-6_18
TABLEAUX
Keywords
Field
DocType
old optimizations,iltp library,propositional prover,propositional intuitionistic logic,previous version,old version,short account,new version,tableau prover pitp,intuitionistic logic
Intuitionistic logic,Discrete mathematics,Computer science,Algorithm,Gas meter prover
Conference
Volume
ISSN
Citations 
4548
0302-9743
1
PageRank 
References 
Authors
0.37
10
3
Name
Order
Citations
PageRank
Alessandro Avellone1637.66
Guido Fiorino29712.71
Ugo Moscato313816.17