In recent years some papers have addressed the problem of the validity in Intuitionistic Propositional Logic (IPL) using the approach proposed by Claessen and Rosén based on reduction to ...Satisfiability Modulo Theories. This approach depends on an initial preprocessing phase that reduces the input formula in the intuitionistic language to an equivalent sequent in the language of clauses. In this paper we present
general clauses
, an extension of the clauses used by Claessen and Rosén, that allow us to define a natural relationship between the semantics of the extended clauses and Kripke semantics. We present a decision procedure for general clauses and we show how to encode intuitionistic formulas in the language of general clauses so to decide IPL. The experimental results show that our implementation in general outperforms the state-of-the-art provers for IPL. In principle general clauses can be used as a target language for other non-classical logics with Kripke semantics, so that our decision procedure can be used to decide them.
Abstract
We propose an internal calculus to check the satisfiability of a set of formulas in ${\boldsymbol {S4}}$. Our calculus directly supports model extraction and is designed so to implement a ...forward proof-search strategy that can be understood as a top-down construction of a model. We prove that the extracted models have minimal height.
The inverse method is a saturation-based theorem-proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here, we ...apply this method to derive the unprovability of a goal formula
G
in Intuitionistic Propositional Logic. To this aim we design a forward calculus
FRJ
(
G
) for Intuitionistic unprovability, which is appropriate for constructively ascertaining the unprovability of a formula
G
by providing a concise countermodel for it; in particular, we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proof-search in
FRJ
(
G
) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.
We address the problem of proof-search in the natural deduction calculus for Intuitionistic propositional logic. Our aim is to improve the usual proof-search procedure where introduction rules are ...applied upwards and elimination rules downwards. In particular, we introduce
Nbu
, a variant of the usual natural deduction calculus for Intuitionistic Propositional Logic, and we show that it can be used as a base for a goal-oriented proof-search procedure. We also show that the implementation of our proof-search procedure is competitive with those based on sequent or tableaux calculi.
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.
PDF
