Efficient Theorem Proving for Conditional Logics with Conditional Excluded Middle

In this work we introduce a labelled sequent calculus for Conditional Logics admitting the axiom of Conditional Excluded Middle (CEM), rejected by Lewis but endorsed by Stalnaker. We also consider some of its standard extensions. Conditional Logics with CEM recently have received a renewed attention and have found several applications in knowledge representation and artificial intelligence. The proposed calculus improves the only existing one, SeqS, where the condition CEM on conditional models is tackled by means of a simple but computationally expensive process of label substitution. Here we propose an alternative calculus avoiding label substitution, where a single rule deals simultaneously with conditional formulas and the CEM axiom. We have implemented the calculi in Prolog following the “lean” methodology, then we have tested the performances of the prover and compared them with those of CondLean, an implementation of SeqS. The performances are promising and better than those of CondLean, witnessing that the proposed calculus provides an effective improvement with respect to the state of the art.