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.

Ferrari, M., Fiorentini, C., Fiorino, G. (2017). JTabWb: A Java Framework for Implementing Terminating Sequent and Tableau Calculi. FUNDAMENTA INFORMATICAE, 150(1), 119-142 [10.3233/FI-2017-1462].

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

Fiorino, G.
2017

Abstract

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.
Articolo in rivista - Articolo scientifico
Java frameworks; Theorem provers;
Java frameworks; Theorem provers; Theoretical Computer Science; Algebra and Number Theory; Information Systems; Computational Theory and Mathematics
English
2017
150
1
119
142
reserved
Ferrari, M., Fiorentini, C., Fiorino, G. (2017). JTabWb: A Java Framework for Implementing Terminating Sequent and Tableau Calculi. FUNDAMENTA INFORMATICAE, 150(1), 119-142 [10.3233/FI-2017-1462].
File in questo prodotto:
File Dimensione Formato  
FIORINO-FUNDAMENTA-INFORMATICAE.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 167.34 kB
Formato Adobe PDF
167.34 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/178677
Citazioni
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 4
Social impact