Labelled Sequent Calculi for Conditional Logics: Conditional Excluded Middle and Conditional Modus Ponens Finally Together

We introduce labelled sequent calculi for Conditional Logics with a selection function semantics. Conditional Logics are a sort of generalization of multimodal logics where modalities are labelled by formulas of the same language. Recently, they received a renewed attention and have found several applications in knowledge representation and artificial intelligence. In a previous work, we have considered the basic system CK and extensions with well known conditions ID, MP, CS and CEM, with the exception of those admitting both conditions CEM and MP, obtaining labelled sequent calculi called SeqS. Here we provide calculi for the whole cube of the extensions of CK generated by the above axioms, including also those with both CEM and MP: the basic idea is that of replacing the rule dealing with CEM in SeqS, which performs a label substitutions in both its premises, by a new one that avoids such a substitution and adopts a conditional formula on the right-hand side of a sequent as its principal formula. We have also implemented the proposed calculi in Prolog following the “lean” methodology, then we have tested the performances of the new prover, called CondLean2022, and compared them with those of CondLean, an implementation of SeqS, on the common systems. The performances of CondLean2022 are promising and seem to be better than those of CondLean, witnessing that the proposed calculi also provide a more efficient theorem prover for Conditional Logics.