We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it directly.

Abstract We investigate intuitionistic modal logics with locally interpreted $$\square $$ □ and $$\lozenge $$ ◊ . The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. Additionally, we present bi-nested calculi for LIK and these extensions, providing both a decision procedure and a procedure of finite countermodel extraction.

Abstract The logic of bringing-it-about (BIAT) aims to capture a notion of agency in which actions are analysed in terms of their results: ‘An agent does something’ means that the agent brings it about that something takes place. Our starting point is the basic BIAT logic as introduced by Elgesem in the ‘90s: this logic contains only a modal operator to express BIAT statements by single agents. Several extensions have been proposed by Elgesem himself and others, notably with the capability operator, coalitions of agents and means-end BIAT statements (i.e. of the form ‘the agent does B by doing A’). We first propose a variant of the neighbourhood semantics, called bi-neighbourhood semantics, for the basic BIAT logic and the mentioned extensions, in which a world is equipped by a set of pairs or neighbourhoods. Differently from the semantics defined in the literature, this reformulation is well suited for countermodel construction. We then introduce modular hypersequent calculi for all logics considered in this work. Our calculi enjoy the fundamental property of cut admissibility, from which it follows their completeness with respect to the axiomatization. Moreover, our calculi provide at the same time a decision procedure, as well as the first practical countermodel extraction procedure: from a single failed proof it is possible to build directly a finite countermodel of the formula under verification in the bi-neighbourhood semantics. By this last result, we obtain constructive proofs of the semantic completeness of the calculi and consequently of the finite model property for all logics.

Abstract We present resolution calculi for the cube of classical non-normal modal logics. The calculi are based on a simple clausal form that comprises both local and global clauses. Any formula can be efficiently transformed into a small set of clauses. The calculi contain uniform rules and provide a decision procedure for all logics. Their completeness is based on a new and crucial notion of inconsistency predicate, needed to ensure the usual closure properties of maximal consistent sets. As far as we know the calculi presented here are the first resolution calculi for this class of logics.

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 We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

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.

We explore the extension of the notion of rational closure to logics lacking the finite model property, considering the logic 𝒮𝒽𝒾𝓆. We provide a semantic characterization of rational closure in 𝒮𝒽𝒾𝓆 in terms of a preferential semantics, based on a finite rank characterization of minimal models. We show that the rational closure of a KB can be computed in EXPTIME based on a polynomial encoding of the rational extension of 𝒮𝒽𝒾𝓆 into entailment in 𝒮𝒽𝒾𝓆. We discuss the extension of rational closure to more expressive description logics.

Nested sequent calculi are a useful generalization of ordinary sequent calculi, where sequents are allowed to occur within sequents. Nested sequent calculi have been profitably used in the area of (multi)-modal logic to obtain analytic and modular proof systems for these logics. In this work, we extend the realm of nested sequents by providing nested sequent calculi for the basic conditional logic CK and some of its significant extensions. We provide also a calculus for Kraus Lehman Magidor cumulative logic C. The calculi are internal (a sequent can be directly translated into a formula), cut-free and analytic. Moreover, they can be used to design (sometimes optimal) decision procedures for the respective logics, and to obtain complexity upper bounds. Our calculi are an argument in favour of nested sequent calculi for modal logics and alike, showing their versatility and power.

We propose a nonmonotonic extension of low complexity Description Logics EL ⊥ and DL-Litecore for reasoning about typicality and defeasible properties. The resulting logics are called EL ⊥ Tmin and DL-LitecTmin. we prove that entailment is in Π p 2 Concerning DL-LitecTmin,. With regard to EL ⊥ Tmin, we first show that entailment remains EXPTIME-hard. Next we consider the known fragment of Left Local EL ⊥ Tmin and we prove that the complexity of entailment drops to Π p 2. 1

Extensions of Description Logics (DLs) to reason about typicality and defeasible inheritance have been largely investigated. In this paper, we consider two such extensions, namely (i) the extension of DLs with a typicality operator T, having the properties of Preferential nonmonotonic entailment P, and (ii) its variant with a typicality operator having the properties of the stronger Rational entailment R. The first one has been proposed in [6]. Here, we investigate the second one and we show, by a representation theorem, that it is equivalent to the approach to preferential subsumption proposed in [3]. We compare the two extensions, preferential and rational, and argue that the first one is more suitable than the second one to reason about typicality, as the latter leads to very unintuitive inferences.

Journal Article Preface Get access Nicola Olivetti Nicola Olivetti Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 20, Issue 1, February 2010, Pages 1–3, https://doi.org/10.1093/logcom/exn057 Published: 01 February 2010

We extend the Description Logic ALC with a "typicality" operator T that allows us to reason about the prototypical properties and inheritance with exceptions. The resulting logic is called ALC + T. The typicality operator is intended to select the "most normal" or "most typical" instances of a concept. In our framework, knowledge bases may then contain, in addition to ordinary ABoxes and TBoxes, subsumption relations of the form "T(C) is subsumed by P", expressing that typical C-members have the property P. The semantics of a typicality operator is defined by a set of postulates that are strongly related to Kraus-Lehmann-Magidor axioms of preferential logic P. We first show that T enjoys a simple semantics provided by ordinary structures equipped with a preference relation. This allows us to obtain a modal interpretation of the typicality operator. We show that the satisfiability of anALC+Tknowledge base is decidable and it is precisely EXPTIME. We then present a tableau calculus for deciding satisfiability of ALC + T knowledge bases. Our calculus gives a (suboptimal) nondeterministic-exponential time decision procedure for ALC + T. We finally discuss how to extend ALC + T in order to infer defeasible properties of (explicit or implicit) individuals. We propose two alternatives: (i) a nonmonotonic completion of a knowledge base; (ii) a "minimal model" semantics for ALC + T whose intuition is that minimal models are those that maximise typical instances of concepts.

We present tableau calculi for the logics of nonmonotonic reasoning defined by Kraus, Lehmann and Magidor (KLM). We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative, and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered and we study their complexity.

We present a tableau calculus for some fundamental systems of propositional conditional logics. We consider the conditional logics that can be characterized by preferential semantics (i.e., possible world structures equipped with a family of preference relations). For these logics, we provide a uniform completeness proof of the axiomatization with respect to the semantics, and a uniform labeled tableau procedure.

In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also show that these calculi can be the base for uniform proof systems. Moreover, we present CondLean, a theorem prover in Prolog for these calculi.

We present two embeddings of Łukasiewicz logicŁinto Meyer and Slaney's Abelian logicA, the logic of lattice-ordered Abelian groups. We give new analytic proof systems forAand use the embeddings to derive corresponding systems forŁ. These include hypersequent calculi, terminating hypersequent calculi, co-NP labeled sequent calculi, and unlabeled sequent calculi.

A uniform proof-theoretic reconstruction of the major nonmonotonic logics is introduced. It consists of analytic sequent calculi where the details of nonmonotonic assumption making are modelled by an axiomatic rejection method. Another distinctive feature of the calculi is the use of provability constraints that make reasoning largely independent of any specific derivation strategy. The resulting account of nonmonotonic inference is simple and flexible enough to be a promising playground for investigating and comparing proof strategies, and for describing the behavior of automated reasoning systems. We provide some preliminary evidence for this claim by introducing optimized calculi, and by simulating an existing tableaux-based method for circumscription. The calculi for skeptical reasoning support concise proofs that may depend on a strict subset of the given theory. This is a difficult task, given the nonmonotonic behavior of the logics.