Abstract Intuitionistic conditional logic, studied by Weiss, Ciardelli and Liu, and Olkhovikov, aims at providing a constructive analysis of conditional reasoning. In this framework, the would and the might conditional operators are no longer interdefinable. The intuitionistic conditional logics considered in the literature are defined by setting Chellas’ conditional logic $$\textsf{CK}$$ CK , whose semantics is defined using selection functions, within the constructive and intuitionistic framework introduced for intuitionistic modal logics. This operation gives rise to a constructive variant of might-free- $$\textsf{CK}$$ CK , which we call "Image missing" , and an intuitionistic variant of $$\textsf{CK}$$ CK , called $$\textsf{IntCK}$$ IntCK . Building on the proof systems defined for $$\textsf{CK}$$ CK and for intuitionistic modal logics, in this paper we introduce a nested calculus for $$\textsf{IntCK}$$ IntCK and a sequent calculus for "Image missing" . Based on the sequent calculus, we define $$\textsf{ConstCK}$$ ConstCK , a conservative extension of Weiss’ logic "Image missing" with the might operator. We introduce a class of models and an axiomatisation for $$\textsf{ConstCK}$$ ConstCK , and extend these result to some extensions of $$\textsf{ConstCK}$$ ConstCK .

In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson’s PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.

Abstract We propose a cut-free cyclic system for transitive closure logic (TCL) based on a form of hypersequents , suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and propositional dynamic logic ( $$\text {PDL}$$ PDL ), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and $$\text {PDL}$$ PDL , thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting ‘alternating traces’ and necessitating a more intricate soundness argument than for traditional cyclic proofs.

Abstract We present hypersequent calculi for the strongest logics in Lewis’ family of conditional systems, characterized by uniformity and total reflexivity. We first present a non-standard hypersequent calculus, which allows a syntactic proof of cut elimination. We then introduce standard hypersequent calculi, in which sequents are enriched by additional structures to encode plausibility formulas and diamond formulas. Proof search using these calculi is terminating, and the completeness proof shows how a countermodel can be constructed from a branch of a failed proof search. We then describe tuCLEVER, a theorem prover that implements the standard hypersequent calculi. The prover provides a decision procedure for the logics, and it produces a countermodel in case of proof search failure. The prover tuCLEVER is inspired by the methodology of leanTAP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.1

Abstract The preferential conditional logic $ \mathbb{PCL} $, introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalizes Lewis’ sphere models for counterfactual logics, is proposed. Soundness and completeness of $ \mathbb{PCL} $ and its extensions with respect to this class of models are proved directly. Labelled sequent calculi for all logics of the family are then introduced. The calculi are modular and have standard proof-theoretical properties, the most important of which is admissibility of cut that entails a syntactic proof of completeness of the calculi. By adopting a general strategy, root-first proof search terminates, thereby providing a decision procedure for $ \mathbb{PCL} $ and its extensions. Finally, semantic completeness of the calculi is established: from a finite branch in a failed proof attempt it is possible to extract a finite countermodel of the root sequent. The latter result gives a constructive proof of the finite model property of all the logics considered.