Abstract This paper considers the bi-modal logic with both $$\Box $$ □ and $$\Diamond $$ ◊ arising from Kripke models with crisp accessibility whose propositions are valued over the standard Gödel algebra [0, 1]. Since this logic lacks the finite model property, we study the logic $$\textbf{GW}^\textrm{c}$$ GW c relying on witnessed Kripke models where, for each modal formula, there is an assignment where the formula without the modality takes the same value as the modal one. We provide a cut-free sequent calculus and we exploit it to prove that $$\textbf{GW}^\textrm{c}$$ GW c is decidable and meets the finite model property. Finally, we explore a connection between the witnessed models and the well-known bi-relational Kripke semantics.

Abstract Intuitionistic Strong Löb logic $$\textsf{iSL}$$ iSL is an intuitionistic modal logic with a provability interpretation. We introduce $$\textsf{GbuSL}_{\Box } $$ GbuSL □ , a terminating sequent calculus for $$\textsf{iSL}$$ iSL with the subformula property. $$\textsf{GbuSL}_{\Box } $$ GbuSL □ modifies the sequent calculus $$\textsf{G3iSL}_{\Box } $$ G 3 iSL □ for $$\textsf{iSL}$$ iSL based on $$\textsf{G3i} $$ G 3 i , by annotating the sequents to distinguish rule applications into an unblocked phase, where any rule can be backward applied, and a blocked phase where only right rules can be used. We prove that, if proof search for a sequent $$\sigma $$ σ in $$\textsf{GbuSL}_{\Box } $$ GbuSL □ fails, then a Kripke countermodel for $$\sigma $$ σ can be constructed.

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 formulaGin Intuitionistic Propositional Logic. To this aim we design a forward calculusFRJ(G) for Intuitionistic unprovability, which is appropriate for constructively ascertaining the unprovability of a formulaGby 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 inFRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.

In this brief note, we outline Mario Ornaghi’s contributions to the field of computational logic to celebrate his 70th birthday.

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.

Following the approaches given in recent works about action languages over description logics, we propose an action formalism based on a constructive information terms semantics for ALC. We discuss how a notion of state can be naturally encoded by this semantics. We address the problems of determining executability of an action, building the state obtained by an action application and checking its consistency: we present an algorithm to solve the latter two problems.

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 abstract we will describe research in progress on the problem of extracting information from proofs. Here we will concentrate our attention on semiconstructive calculi, which is a kind of calculus that is of interest in the framework of program synthesis and formal verification. We will discuss the notion of uniformly semiconstructive calculus, introduce our information extraction mechanism and apply it to two calculi extending Intuitionistic Arithmetic.

Abstract A proof is given that the set of maximal intermediate propositional logics with the disjunction property and the set of maximal intermediate predicate logics with the disjunction property and the explicit definability property have the power of continuum. To prove our results, we introduce various notions which might be interesting by themselves. In particular, we illustrate a method to generate wide sets of pairwise “constructively incompatible constructive logics”. We use a notion of “semiconstructive” logic and define wide sets of “constructive” logics by representing the “constructive” logics as “limits” of decreasing sequences of “semiconstructive” logics. Also, we introduce some generalizations of the usual filtration techniques for propositional logics. For instance, “fitrations over rank formulas” are used to show that any two different logics belonging to a suitable uncountable set of “constructive” logics are “constructively incompatible”.