From input/output logics to conditional logics via sequents -- with provers

DOI10.1007/978-3-030-86059-2_9MaRDI QIDQ2142070zbMATH OpenOpenAlexFDO

Authors Björn Lellmann

Publication date 25 May 2022

Full work available at URL https://doi.org/10.1007/978-3-030-86059-2_9

zbMATH Keywords

conditional logicdeontic logicI/O logicsequent systems

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A sequent calculus and a theorem prover for standard conditional logics
• Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
• Generic methods for formalising sequent calculi applied to provability logic
• scientific article; zbMATH DE number 218517
• Nested sequent calculi for conditional logics
• On sequent calculi for intuitionistic propositional logic.
• CondLean: a theorem prover for conditional logics
• Proving structural properties of sequent systems in rewriting logic
• A logic program for transforming sequent proofs to natural deduction proofs
• scientific article; zbMATH DE number 589741

Cites work

• A standard internal calculus for Lewis' counterfactual logics
• Analytic tableaux calculi for KLM logics of nonmonotonic reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods
• Conditional and preferential logics. Proof methods and theorem proving.
• Cut elimination for shallow modal logics
• Generic modal cut elimination applied to conditional logics
• Goal-directed decision procedures for input/output logics
• scientific article; zbMATH DE number 3670430 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 7085150 (Why is no real title available?)
• scientific article; zbMATH DE number 6741901 (Why is no real title available?)
• I/O logic in HOL
• Input/output logic with a consistency check -- the case of permission
• Input/output logics
• Intuitionistic basis for input/output logic
• KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning
• lean\(T^ AP\): Lean tableau-based deduction
• Modularisation of sequent calculi for normal and non-normal modalities
• NESCOND: an implementation of nested sequent calculi for conditional logics
• Nested sequent calculi for normal conditional logics
• Nonmonotonic reasoning, preferential models and cumulative logics
• Normative Consequence: The Problem of Keeping It Whilst Giving It up
• On the complexity of input/output logic
• Permission from an input/output perspective
• Sequent calculi for propositional nonmonotonic logics
• Sequent Systems for Lewis’ Conditional Logics
• Standard sequent calculi for Lewis' logics of counterfactuals
• VINTE: an implementation of internal calculi for Lewis' logics of counterfactual reasoning

Cited in

(4)

• Permission from an input/output perspective
• Theorem proving for conditional logics: CondLean and GOALDUCK
• Subordination algebras as semantic environment of input/output logic
• A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs

Describes a project that uses

Uses Software

• CondLean
• KLMLean
• NESCOND
• VINTE

This page was built for publication: From input/output logics to conditional logics via sequents -- with provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2142070)