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 p aper 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.

It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the naïve goal-oriented proof-search strategy, consisting in applying the rules of the calculus bottom up until possible, can generate branches of infinite length. The usual solution to this problem is to support the proof-search procedure with a loop checking mechanism that prevents the generation of infinite branches by storing and analyzing some information regarding the branch under development. In this article, we propose a new technique based on evaluation functions. An evaluation function is a lightweight computational mechanism that, analyzing only the current goal of the proof search, allows one to drive the application of rules to guarantee termination and to avoid useless backtracking. We describe an evaluation-driven proof-search procedure that given a sequent σ returns either a G3i-derivation of σ or a countermodel for σ. We prove that such a procedure is terminating and correct, and that the depth of the G3i-trees generated during proof search is quadratic in the size of σ. Finally, we discuss the overhead time introduced by evaluation functions in the proof-search procedure.

The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this article we introduce some simplification rules for Intuitionistic propositional logic that try to replace a formula with an equi-satisfiable “simpler” one with the aim to reduce the search space. Our results are proved via semantical techniques based on Kripke models. We also provide an empirical evaluation of their impact on implementations.

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation.

In this article we study the complexity of disjunction property for intuitionistic logic, the modal logicsS4,S4.1, Grzegorczyk logic, Gödel-Löb logic, and the intuitionistic counterpart of the modal logicK. ForS4we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require proving structural properties of the calculi in hand, such as the cut-elimination theorem or the normalization theorem. This is a key point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known.

In this paper we present duplication‐free tableau calculi for three propositional intermediate interpolable logics, namely the logic characterized by rooted Kripke models with depth two at most, the logic characterized by rooted Kripke models with two final elements at most and depth two at most and the logic characterized by rooted Kripke models with a final element at most (also known as Jankov Logic). Using such calculi we define a O(n)‐SPACE decision procedure for the second logic and a O(n log n)‐SPACE decision procedure for each of the other two logics.