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 propose a nonmonotonic Description Logic of typicality able to account for the phenomenon of the combination of prototypical concepts. The proposed logic relies on the logic of typicality $\mathcal{A}\mathcal{L}\mathcal{C}+{\mathbf{T}}_{\mathbf{R}}$, whose semantics is based on the notion of rational closure, as well as on the distributed semantics of probabilistic Description Logics, and is equipped with a cognitive heuristic used by humans for concept composition. We first extend the logic of typicality $\mathcal{A}\mathcal{L}\mathcal{C}+{\mathbf{T}}_{\mathbf{R}}$ by typicality inclusions of the form $p::\mathbf{T}(C)⊑D$, whose intuitive meaning is that ‘we believe with degree $p$ about the fact that typical Cs are Ds’. As in the distributed semantics, we define different scenarios containing only some typicality inclusions, each one having a suitable probability. We then exploit such scenarios in order to ascribe typical properties to a concept $C$ obtained as the combination of two prototypical concepts. We also show that reasoning in the proposed Description Logic is ExpTime-complete as for the underlying standard Description Logic $\mathcal{A}\mathcal{L}\mathcal{C}$.

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 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.