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 present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SAT-solver. Basically, it is obtained by adding a restart operation to the system by Claessen and Rosén, thus we call our implementation . We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform and other state-of-the-art provers.

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.

Intuitionistic Propositional Logic is complete w.r.t. Kripke semantics: if a formula is not intuitionistically valid, then there exists a finite Kripke model falsifying it. The problem of obtaining concise models has been scarcely investigated in the literature. We present a procedure to generate minimal models in the number of worlds relying on Answer Set Programming (ASP).

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

LogicaComputazionale, CILC 2016) that was hosted by the Università degli Studi di Milano-Bicocca, Italy, from June 20th to June 22th, 2016.The event was the thirty-first edition of the annual meeting of the Italian Association for Logic Programming (GULP, Gruppo Ricercatori e Utenti di Logic Programming).Since its first edition, the annual conference organized by GULP is the main occasion of meeting and exchanging ideas and experiences among Italian researchers who work in the field of Computational Logic.During the years, this meeting has extended its horizons from the area of Logic Programming to the area of Computational Logic in general, including aspects of Artificial Intelligence and Deductive Databases.The program of CILC 2016 included 21 technical papers accepted for presentation and a few demos.Paper selection was made by peer reviewing.vi iii Description Logic ALC based on the combination of a typicality operator and the well-established non-monotonic mechanism of rational closure, which allows one to deal with prototypical properties and defeasible inheritance.Martin Sticht presents a multi-agent version of dialogical logic that corresponds more to multiconclusion sequent calculi for propositional intuitionistic logic rather than single-conclusion ones, which are related to two-player dialogues.We would like to thank the Department of Computer

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.

Focusing is a proof-theoretic device to structure proof search in the sequent calculus: it provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured in two separate and disjoint phases. Although stemming from proof-search cons iderations, focusing has not been thoroughly investigated in actual theorem proving, in particular w.r.t. termination. We present a contraction-free (and hence terminating) focused multi-succedent sequent calculus for propositional intuitionistic logic, which refines the G4ip calculus in the tradition of Vorob’ev, Hudelmeier and Dyckhoff. We prove completeness of the calculus semantically and argue that this offers a viable alternative to other more syntactical means.

We present a contraction-free sequent calculus GS4 for the modal logic S4 such that all the rules are decreasing and enjoy the subformula property. We also introduce a refutation calculus RS4 with the same properties of GS4. We provide a proof search algorithm that, given a sequent σ, returns either a proof of σ in GS4 or a refutation of σ in RS4. From a refutation of σ, we can generate an S4-model of σ.

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 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 In [8] it is proved that all the intermediate logics axiomatizable by formulas in one variable, except four of them, are not strongly complete. We considerably improve this result by showing that all the intermediate logics axiomatizable by formulas in one variable, except eight of them, are not strongly ω-complete. Thus, a definitive classification of such logics with respect to the notions of canonicity, strong completeness, ω-canonicity and strong ω-completeness is given.