JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi

• Autorzy: Ferrari M. , Fiorentini C. , Fiorino G.

Identyfikatory

DOI

10.3233/FI-2017-1462

• Języki publikacji: EN

Abstrakty

EN

JTabWb is a Java framework for developing provers based on sequent or tableau calculi. It provides a generic engine which searches for proof of a given goal driven by a user-defined prover. The user is required to define the components of a prover by implementing suitable Java interfaces. In this paper we describe the structure of the framework and the role of its components through a running example. To show the generality of the framework we review some of the provers implemented in JTabWb. Finally, to corroborate the fact that the framework can be used to generate efficient provers, we compare the performances of one of the implemented provers with the state-of-the-art provers for Intuitionistic Propositional Logic.

Słowa kluczowe

EN

theorem provers; Java frameworks

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 1
• Strony: 119--142
• Opis fizyczny: Bibliogr. 24 poz., tab., wykr.

Twórcy

autor

Ferrari M.

• Università degli Studi dell’Insubria, Via Mazzini, 5, 21100, Varese, Italy

autor

Fiorentini C.

• Università degli Studi di Milano, Via Comelico, 39, 20135, Milano, Italy

autor

Fiorino G.

• Università degli Studi di Milano-Bicocca, Viale Sarca, 336, 20126, Milano, Italy

Bibliografia

• [1] Abate P, Goré R. The Tableau Workbench, ENTCS, 2009; 231: 55-67. doi: 10.1016/j.entcs.2009.02.029.
• [2] Bertot Y, Casteran P, Huet G, Paulin-Mohring C. Interactive theorem proving and program development. - Coq’Art: the calculus of inductive constructions, Texts in Theoretical Computer Science, Springer, 2004. doi: 10.1007/978-3-662-07964-5.
• [3] Calin G, Myers RSR. Pattinson D, Schröder L. CoLoSS: The Coalgebraic Logic Satisfiability Sover, ENTCS, 2009; 231: 41-54. doi: 10.1016/j.entcs.2009.02.028.
• [4] Ferrari M. Fiorentini C. Goal-oriented proof-search in natural deduction for Intuitionistic propositional logic, Submitted, 2015.
• [5] Ferrari M., Fiorentini C. Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, TABLEAUX 2015 (H. D. Nivelle, Ed.), 9323, Springer International Publishing, 2015. doi: 10.1007/978-3-319-24312-2_17.
• [6] Ferrari. M., Fiorentini C., Fiorino, G.: A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications, Journal of Applied Non-Classical Logics, 19 (2), 2009, 149-166.
• [7] Ferrari M., Fiorentini C., Fiorino G. Fcube: An Efficient Prover for Intuitionistic Propositional Logic, Proc. LPAR 2010 (C. G. Fermüller, A. Voronkov. Eds.), LNCS 6397. Springer, 2010. doi: 10.1007/978-3-642-16242-8_21.
• [8] Ferrari M, Fiorentini C., Fiorino G. Simplification Rules for Intuitionistic Propositional Tableaux, ACM Transactions on Computational Logic (TOCL). 2012; 13 (2): 14:1-14:23. doi: 10.1145/2159531.2159536.
• [9] Ferrari M, Fiorentini C., Fiorino G. Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models, Journal of Automated Reasoning, 2013; 51 (2): 129-149. doi: 10.1007/s10817-012-9252-7.
• [10] Ferrari M, Fiorentini C., Fiorino G. A terminating evaluation-driven variant of G3i, Proc. TABLEAUX 2013 (D. Galmiche. D. Larchey-Wendling, Eds.), LNCS 8123, Springer, 2013 pp. 104-118. doi: 10.1007/978-3-642-40537-2_11.
• [11] Ferrari M, Fiorentini C., Fiorino G. An evaluation-driven decision procedure for G3i, ACM Transactions on Computational Logic (TOCL), 2015; 6 (1): 8:1-8:37. doi: 10.1145/2660770.
• [12] Gasquet O, Herzig A, Longin D, Sahade M. LoTREC: Logical Tableaux Research Engineering Companion, Proc. TABLEAUX 2005 (B. Beckert. Ed.), LNCS 3702, 2005.
• [13] Goré R, Thomson J., Wu J A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description, Proc. IJCAR 2014 (S. Demri, D. Kapur, C. Weidenbach, Eds.), LNCS 8562, Springer, 2014 pp. 262-268. doi: 10.1007/978-3-319-08587-6_19.
• [14] Gorín D., Pattinson D., Schröder L, Widmann F., Wißmann T. Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description), IJCAR 2014 (S. Demri, D. Kapur, C. Weidenbach, Eds.), 8562, Springer, 2014 pp. 396-402. doi: 10.1007/978-3-319-08587-6_31.
• [15] Howe JM Two Loop Detection Mechanisms: A Comparison. Proc. TABLEAUX 1997 (D. Galmiche, Ed.), LNCS 1227. Springer. 1997 pp 188-200 doi: 10.1007/BFb0027414.
• [16] Hustadt U., Schmidt R Simplification and backjumping in modal tableau, Proc. TABLEAUX 1998 (H. C. M. de Swart, Ed.), LNCS 1397, Springer, 1998 pp. 187-201. URL http://dl.acm.org/citation.cfm?id=646889.709107.
• [17] McLaughlin S., Pfenning F Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic, Proc. LPAR 2008 (I. Cervesato, H. Veith, A. Voronkov, Eds.), LNCS 5330, 2008 pp. 174-181. doi: 10.1007/978-3-540-89439-1_12.
• [18] Miglioli P., Moscato U, Ornaghi M. Refutation systems for propositional modal logics, TABLEAUX 1995 (P. Baumgartner, R. Hänle, J. Posegga. Eds.), 918. Springer-Verlag, 1995 pp. 95-105. doi: 10.1007/3-540-59338-1_30.
• [19] Owre S, Rushbv JM, Shankar N. PVS: A Prototype Verification System. Proc. CADE 1992 (D. Kapur, Ed.), LNCS 607, 1992 pp. 748-752. URL http://www.csl.sri.com/papers/cade92-pvs/.
• [20] Paulson LC. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), vol. 828 of LNCS, Springer, 1994. ISBN-10: 3540582444, 13: 9783540582441.
• [21] Raths T., Otten J, Kreitz C. The ILTP Problem Library for Intuitionistic Logic, Journal of Automated Reasoning. 2007; 31: 261-271.
• [22] Sieg W, Byrnes I. Normal Natural Deduction Proofs (in classical logic), Studia Logica, 1998; 60 (1): 67-106. doi: 10.1023/A:1005091418752.
• [23] Tishkovsky D, Schmidt R, Khodadadi M. The Tableau Prover Generator MetTeL2, Proc. JELIA 2012 (L. F. del Cerro et al., Ed.), LNCS 7519, 2012 pp. 492-495. doi: 10.1007/978-3-642-33353-8_41.
• [24] Troelstra A, Schwichtenberg H. Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, 2nd edition, Cambridge University Press, 2000. ISBN-10: 0521779111, 13: 978-0521779111.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).