2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/32263In this paper we present a cut-free sequent calculus, called SeqS, for some standard conditional logics, namely CK, CK+ID, CK+MP and CK+MP+ID. The calculus uses labels and transition formulas and can be used to prove decidability and space complexity bounds for the respective logics. We also present CondLean, a theorem prover for these logics implementing SeqS calculi written in SICStus Prolog.45 pages with 2 figures, uses prooftree.styLogic in Computer ScienceArtificial IntelligenceD.1.6; F.4.1; I.2.3text