A Sequent Calculus and a Theorem Prover for Standard Conditional Logics

TL;DR

This paper introduces a cut-free sequent calculus named SeqS for standard conditional logics and develops CondLean, a theorem prover implementing SeqS in SICStus Prolog, facilitating decision procedures.

Contribution

It presents the first sequent calculus for multiple standard conditional logics and implements a theorem prover based on it, advancing automated reasoning in this domain.

Findings

Decidability and space complexity bounds established for the logics

Implementation of a theorem prover in SICStus Prolog

Formal proof system for standard conditional logics

Abstract

In 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.