Affiliations: [a] Aix Marseille Université, CNRS, ENSAM, Université de Toulon, LSIS UMR 7296, Marseille, France | [b] Dipartimento di Informatica, Universitá degli Studi di Torino, c.so Svizzera 185, Torino, Italy
Correspondence:
[*]
Corresponding author: Gian Luca Pozzato, Dipartimento di Informatica, Universitá degli Studi di Torino, c.so Svizzera 185, 10149 Torino, Italy. Tel. +39 011 670 6848; Fax: +39 011 75 16 03; E-mail: gianluca.pozzato@unito.it.
Note: [1] The author is partially supported by the Project “ExceptionOWL: Nonmonotonic Extensions of Description Logics and OWL for defeasible inheritance with exceptions”, progetti di ricerca di Ateneo anno 2014, Call 01 “Excellent Young PI”, Torino_call2014_L1_111, Università di Torino and Compagnia di San Paolo.
Abstract: In this paper we focus on proof methods and theorem proving for normal conditional logics, by describing nested sequent calculi as well as a theorem prover for them. We first present some nested sequent calculi, recently introduced, for the basic conditional logic CK and some of its significant extensions with axioms ID, MP and CEM. We also describe a calculus for the flat fragment of the conditional logic CK+CSO+ID, which corresponds to Kraus, Lehmann and Magidor’s cumulative logic C. The calculi are internal, cut-free and analytic. Next, we describe NESCOND, a Prolog implementation of these calculi in the style of leanTAP. We finally present an experimental comparison between our theorem prover NESCOND and other known theorem provers for conditional logics. Our tests show that the performances of NESCOND are promising and in all cases better, with the only exception of systems including CEM, than those ones of the other provers. The program NESCOND, as well as all the Prolog source files, are available at http://www.di.unito.it/~pozzato/nescond/.
