Free variable tableaux for propositional modal logics

DOI10.1007/BFB0027407MaRDI QIDQ4610317zbMATH OpenOpenAlexFDO

Authors Bernhard Beckert, Rajeev Goré

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bfb0027407

zbMATH Keywords

modal logicuniversal variablepropositional modal logicfree variablerule application

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic programming (68N17) Mechanization of proofs and logical operations (03B35)

Recommendations

• Free-variable tableaux for propositional modal logics
• TABLEAUX: A general theorem prover for modal logics
• First-order modal tableaux
• Ground and free-variable tableaux for variants of quantified modal logics
• Almost duplication-free tableau calculi for propositional lax logics

Cites work

• scientific article; zbMATH DE number 3125693 (Why is no real title available?)
• scientific article; zbMATH DE number 140385 (Why is no real title available?)
• scientific article; zbMATH DE number 1028821 (Why is no real title available?)
• scientific article; zbMATH DE number 1140671 (Why is no real title available?)
• scientific article; zbMATH DE number 1489626 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 932649 (Why is no real title available?)
• Efficient loop-check for backward proof search in some non-classical propositional logics
• Grafting modalities onto substructural implication systems
• Proof methods for modal and intuitionistic logics
• SETHEO: A high-performance theorem prover
• Strongly analytic tableaux for normal modal logics
• Tableau methods for modal and temporal logics
• The tableau-based theorem prover 3 T A P Version 4.0
• lean\(T^ AP\): Lean tableau-based deduction

Cited in

(15)

• Almost duplication-free tableau calculi for propositional lax logics
• First-order modal tableaux
• Free-variable semantic tableaux for the logic of fuzzy inequalities
• Ground and free-variable tableaux for variants of quantified modal logics
• scientific article; zbMATH DE number 1189105 (Why is no real title available?)
• Tableaux methods for access control in distributed systems
• Modal definability of first-order formulas with free variables and query answering
• Tableau calculus for local cubic modal logic and its implementation
• Free-variable tableaux for propositional modal logics
• IeanCOP: lean connection-based theorem proving
• Free-variable tableaux for monotonic preorders
• Tableau methods for a logic with term declarations
• A variable-free logic for mass terms
• Labelled deduction for the guarded fragment
• Labelled modal tableaux

Describes a project that uses

Uses Software

• 3TAP
• leanTAP
• SETHEO

This page was built for publication: Free variable tableaux for propositional modal logics

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