A sequent calculus and a theorem prover for standard conditional logics
From MaRDI portal
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.
Recommendations
Cited in
(38)- Hypersequent calculi for Lewis' conditional logics with uniformity and reflexivity
- M-calculus -- a sequent method for automatic theorem proving
- Embedding and automating conditional logics in classical higher-order logic
- Sequent calculi for choice logics
- From input/output logics to conditional logics via sequents -- with provers
- Cut-elimination for quantified conditional logic
- A sequent calculus for a logic of contingencies
- Nested sequent calculi for normal conditional logics
- Admissibility of cut in coalgebraic logics
- Nested sequent calculi for conditional logics
- Sequent Systems for Lewis’ Conditional Logics
- Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra
- A conditional constructive logic for access control and its sequent calculus
- Cut elimination for shallow modal logics
- A Focused Sequent Calculus for Higher-Order Logic
- NESCOND: an implementation of nested sequent calculi for conditional logics
- Natural deduction calculi and sequent calculi for counterfactual logics
- In all, but finitely many, possible worlds: model-theoretic investigations on `\textit{overwhelming majority}' default conditionals
- A sequent calculus for preferential conditional logic based on neighbourhood semantics
- Theorem proving for conditional logics: CondLean and GOALDUCK
- scientific article; zbMATH DE number 1086653 (Why is no real title available?)
- Terminating sequent calculi for proving and refuting formulas in S4
- CondLean: a theorem prover for conditional logics
- A representation of proper BC domains based on conjunctive sequent calculi
- Automated Reasoning with Analytic Tableaux and Related Methods
- A Gentzen-type calculus of sequents for single-operator propositional logic
- Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning
- Labelled sequent calculi for logics of strict implication
- A sequent calculus for first-order logic formalized in Isabelle/HOL
- Cut elimination in coalgebraic logics
- Proof analysis in intermediate logics
- From modal sequent calculi to modal resolution
- Uniform Lyndon interpolation for basic non-normal modal and conditional logics
- Sequent calculi and an efficient theorem prover for conditional logics with selection function semantics
- Non-iterative modal resolution calculi
- Strict-tolerant conditional logics
- A coding method for a sequent calculus of propositional logic
- A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs
This page was built for publication: A sequent calculus and a theorem prover for standard conditional logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277787)
