Abstract dell'evento

In ordinary life as well as in scientific theorizing, nonmonotonic reasoning allows to draw plausible conclusions under incomplete and uncertain information. In this talk, we present a novel proof-theoretic approach to nonmonotonic reasoning, based on the combination of sequents and antisequents — i.e., sequents for unprovability — into suitable hybrid Gentzen-style calculi.

In the first part, we explore abductive reasoning — i.e., the kind of nonmonotonic reasoning which involves finding the missing premise of an “unsaturated” deductive inference. We present a hybrid sequent calculus for classical propositional logic to define a procedure for identifying the set of analytic hypotheses that a rational agent would be expected to select as explanans when presented with an abductive problem. Specifically, we show that this set may not include the deductively minimal hypothesis due to the presence of redundant information, and we establish a completeness result for the set of all analytic hypotheses. Furthermore, we propose a deductive criterion for differentiating between the best explanans candidates and other hypotheses.

In the second part, we investigate default reasoning — i.e., the kind of nonmonotonic reasoning which allows to make additional extra-logical assumptions unless there is explicit evidence to the contrary. We introduce hybrid hypersequent calculi for propositional default logics, where distinct extra-logical rules directly capture default rules, and parallel composition of sequents and antisequents formalizes contrary updating on the conclusions of extra-logical rules. We establish the admissibility of structural rules and the invertibility of logical rules, showing that cut-free proofs exhibit a weakened form of analyticity. Next, we prove that specific hybrid hypersequent calculi are sound and weakly complete with respect to credulous consequence based on \L ukaszewicz extensions. Moreover, we propose a hypersequent-based decision method for skeptical consequence which circumvents the need for early computation of all extensions by assessing provability against finite sequences of abductive inferences.

Finally, we further illustrate the potential of our proof-theoretic framework by sketching applications to other variants of default logic as well as to (base-generated) AGM belief revision.