Abstract In this paper we consider the intuitionistic non-Fregean sentential calculus with Suszko’s identity ($\mathsf{ISCI}$). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for $\mathsf{ISCI}$, called Topological Beth (${\mathsf{TB}}$) models, that can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. From this semantical study we define a family of sound and cut-free complete labelled calculi that capture both the Kripke and the ${\mathsf{TB}}$ semantics. Using a key property of the forcing relation in ${\mathsf{TB}}$ models, called regularity, we show termination and decidability results. Finally we discuss the automation of the proof search in one of the labelled calculi and its implementation.

In this paper we consider the intuitionistic sentential calculus with Suszko’s identity (ISCI). After recalling the basic concepts of the logic and its associated Hilbert proof system, we introduce a new sound and complete class of models for ISCI which can be viewed as algebraic counterparts (and extensions) of sheaf-theoretic topological models of intuitionistic logic. We use this new class of models, called Beth semantics for ISCI, to derive a first labelled sequent calculus and show its adequacy w.r.t. the standard Hilbert axiomatization of ISCI. This labelled proof system, like all other current proof systems for ISCI that we know of, does not enjoy the subformula property, which is problematic for achieving termination. We therefore introduce a second labelled sequent calculus in which the standard rules for identity are replaced with new special rules and show that this second calculus admits cut-elimination. Finally, using a key regularity property of the forcing relation in Beth models, we show that the eigenvariable condition can be dropped, thus leading to the termination and decidability results.

Abstract Separation logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. It is successful for program verification as an assertion language to state properties about memory heaps using Hoare triples. Most of the proof systems and verification tools for ${\textrm{SL}}$ focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof systems that go beyond symbolic heaps are purely syntactic or labelled systems dedicated to some fragments of ${\textrm{SL}}$ and they mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. In this work, we present a labelled proof system, called ${\textrm{G}_{\textrm{SL}}}$, that allows both the definition of cyclic proofs with arbitrary inductive predicates and the full set of SL connectives. We prove its soundness and show that we can derive in ${\textrm{G}_{\textrm{SL}}}$ the built-in rules for data structures of another non-cyclic labelled proof system and also that ${\textrm{G}_{\textrm{SL}}}$ is strictly more powerful than that system.

This special issue of the Journal of Automated Reasoning is dedicated to selected papers presented at the 9th Joint Conference on Automated Reasoning (IJCAR 2018), held between July 14 and July 17, 2018 in Oxford, UK, as part of the Federated Logic Conference (FLOC) 2018.IJCAR is the premier international joint conference on all topics in automated reasoning and merges three leading events in automated reasoning: CADE (Conference on Automated Deduction), FroCoS (Symposium on Frontiers of Combining Systems), and TABLEAUX (Conference on Analytic Tableaux and Related Methods).The papers selected for this special issue underwent a two-round reviewing process.In the first round, the papers had been reviewed and accepted by at least three reviewers as part of the IJCAR 2018 reviewing process.We invited authors of top rated papers in the proceedings as evaluated by the reviewers to submit revised and extended versions of their papers to this special issue.In the second round, the submitted extended papers went through the reviewing process of the Journal of Automated Reasoning.Each paper was reviewed by two reviewers.The seven selected papers in this special issue cover a wide spectrum of topics in Automated Reasoning, from proof theory and theorem proving to formalization and mechanization of completeness or decidability results, from proof systems to analysis of complexity and decidability, from automated reasoning to the production of stateful ML programs together with proofs of correctness, from extensions of model checking techniques to the verification of some parameterized systems.The paper "Formalizing Bachmair and Ganzinger's Ordered Resolution Prover" presents a formalization of the first half of Bachmair and Ganzinger's chapter on resolution theorem proving in Isabelle/HOL, providing a refutationally complete first-order prover based on ordered resolution with literal selection.It proposes general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition.The paper "Constructive Decision via Redundancy-free Proof-Search" presents a constructive account of Kripke-Curry's method used to establish the decidability of Implicational Relevance Logic (R → ).The method is mechanized in axiom-free Coq, with the replacement of Kripke/Dickson's lemma by a constructive form of Ramsey's theorem and of König's B

Abstract We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents’ local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI’s resource semantics—we introduce BI and its resource semantics at some length—with epistemic agency. We illustrate the use of the logic in systems modelling by discussing some examples about access control, including semaphores, using resource tokens. We also give a labelled tableaux calculus and establish soundness and completeness with respect to the resource semantics.

Abstract We define a Public Announcement Separation Logic (PASL) that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying its semantics and illustrating its interest for modelling systems, we provide a sound and complete tableau calculus that deals with resource, agent and announcement constraints and give also a countermodel extraction method.

The logic of Bunched implications (BI), and its Boolean version (Boolean BI), are logics that allow us to express properties on resources and to provide logical frameworks for the so-called separation logics. In this article, we study a new modal separation logic that extends Boolean BI with two kinds of modalities, to deal with resources having dynamic properties (which depend on the current state of a system) and also to capture some resource evolutions or transformations. We show how we can model concurrent processes manipulating resources, and we provide a sound and complete tableau calculus, with a counter-model extraction method, for proving properties expressed in this logic.

Logics for Resources, Processes, and Programs (LRPP) is an occasional series of international workshops which aims to explore the current state of logical and semantic approaches to reasoning about the programs that implement the processes that manipulate system resources in order to deliver services. LRPP is concerned with ideas that range from purely logical and semantic work that bears upon the foundations of system modelling through to implemented tools that support formal reasoning about programs and systems. This Special Issue of the Journal of Logic and Computation comprises a selection of papers inspired by the 2013 LRPP workshop, held in association with the Tableaux 2013 conference in Nancy, France and submitted from an open call for papers following the workshop. There are six papers in this special issue, mostly concerned with theoretical logical and semantic aspects of concepts that are of significance in systems of interacting agents. The paper by Nguyen, Alechina, Logan and Rakib, entitled ‘Resource-bounded alternating time temporal logic’, is concerned with reasoning about coalitional ability. As there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL), the authors define a logic for reasoning about coalitional ability under resource constraints. They extend ATL with costs of actions and hence of strategies, and give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL), and a model-checking algorithm for it.

In this article we define label-free sequent calculi for the intuitionistic modal logics obtained from the combinations of the axioms T , B , 4 and 5. These calculi are based on a multi-contextual sequent structure, called Tree-sequent, which allows us to define such calculi for such intuitionistic modal logics. From the calculi defined for the IK , IT , IB4 and ITB logics, we also provide new decision procedures and alternative syntactic proofs of decidability.

Didier Galmiche, Stéphane Graham-Lengrand; Special Issue on Computational Logic in Honour of Roy Dyckhoff, Journal of Logic and Computation, Volume 26, Iss

We present a logic of separating modalities, LSM, that is based on Boolean BI. LSM's modalities, which generalize those of S4, combine, within a quite general relational semantics, BI's resource semantics with modal accessibility. We provide a range of examples illustrating their use for modelling. We give a proof system based on a labelled tableaux calculus with countermodel extraction, establishing its soundness and completeness with respect to the semantics.

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered the core of separation and spatial logics. For this, we define a complete phase semantics suitable for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out the elementary fragment of ILL, which is both undecidable and complete for trivial phase semantics. Thus, we obtain the undecidability of BBI.

We solve the open problem of the decidability of Boolean BI logic (BBI), which can be considered as the core of separation and spatial logics. For this, we define a complete phase semantics for BBI and characterize it as trivial phase semantics. We deduce an embedding between trivial phase semantics for intuitionistic linear logic (ILL) and Kripke semantics for BBI. We single out a fragment of ILL which is both undecidable and complete for trivial phase semantics. Therefore, we obtain the undecidability of BBI.

Separation logic (SL) is often presented as an assertion language for reasoning about mutable data structures. As recent results about verification in SL have mainly been achieved from a model-checking point of view, our aim in this article is to study SL from a complementary proof-theoretic perspective in order to provide results about proof search in SL. We begin our study with a fragment of SL, denoted SLP, where first-order quantifiers, variables and equality are removed. We first define specific structures, called resource graphs, that capture SLP models by considering heaps as resources via a labelling process. We then provide a tableau calculus that allows us to build such resource graphs from which either proofs, or countermodels can be generated. We finally prove soundess, completeness and termination of our tableau calculus before discussing extensions to various fragments of SL (including full SL) and the related decidability issues.

The logic of Bunched Implications, through both its intuitionistic version (BI) and one of its classical versions, called BooleanBI(BBI), serves as a logical basis to spatial or separation logic frameworks. InBI, the logical implication is interpreted intuitionistically whereas it is generally interpreted classically in spatial or separation logics, as inBBI. In this paper, we aim to give some new insights into the semantic relations betweenBIandBBI. Then we propose a sound and complete syntactic constraints based framework for the Kripke semantics of bothBIandBBI, a sound labelled tableau proof system forBBI, and a representation theorem relating the syntactic models ofBIto those ofBBI. Finally, we deduce as our main, and unexpected, result, a sound and faithful embedding ofBIintoBBI.

In this article, we propose a new data structure, called resource tree, that is a node-labelled tree in which nodes contain resources which belong to a partial monoid. We define the resource tree model and a new separation logic (BI-Loc) that extends the Bunched Implications logic (BI) with a modality for locations. In addition, we consider quantifications on locations and paths and then we study decidability by model-checking in these models and logics. Moreover, we define a language to deal with resource trees and also an assertion logic derived from BI-Loc. Then soundness and completeness issues are studied, and we show how the model and its associated language can be used to manage heap structures and also permission accounting.

The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource that is rich enough, for example, to form the logical basis for ‘pointer logic’ and ‘separation logic’ semantics for programs that manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI's tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, , the challenge consists in dealing with BI's Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. Then, from these results, we can define a new resource semantics of BI, based on partially defined monoids, and prove that this semantics is complete. Such a semantics, based on partiality, is closely related to the semantics of BI's (intuitionistic) pointer and separation logics. Returning to the tableaux calculus, we propose a new version with liberalised rules for which the countermodels are closely related to the topological Kripke semantics of BI. As consequences of the relationships between semantics of BI and resource tableaux, we prove two new strong results for propositional BI: its decidability and the finite model property with respect to topological semantics.

In this paper, we study semantic labelled tableaux for the propositional Bunched Implications logic (BI) that freely combines intuitionistic logic (IL) and multiplicative intuitionistic linear logic (MILL). BI is a resource-aware logic that captures interferences between resources and it is well suited, because of its resource-based sharing interpretation, for reasoning about mutable data structures. We propose a labelled tableau calculus for BI⊥1 based on particular labels and constraints. We prove the soundness and completeness of this calculus w.r.t. the Kripke resource semantics with emphasis on countermodel construction. In addition, we prove the finite model property and as a consequence the decidability of BI⊥. Moreover, we analyse some algorithmic aspects of the tableau construction by providing a free variable variant of the calculus. We also develop the restrictions to IL and MILL that provide new tableau methods for both logics with generation of countermodels.