Free-variable tableaux for propositional modal logics

DOI10.1023/A:1013886427723MaRDI QIDQ5955622zbMATH OpenOpenAlexFDO

Authors Bernhard Beckert, Rajeev Goré

Publication date 3 September 2002

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1013886427723

zbMATH Keywords

automated decuctionfree-variable tableauxpropositional modal logicstheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Free variable tableaux for propositional modal logics
• First-order modal tableaux
• Ground and free-variable tableaux for variants of quantified modal logics
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• TABLEAUX: A general theorem prover for modal logics

Cited in

(18)

• The liberalized -rule in free variable semantic tableaux
• Rule refinement for semantic tableau calculi
• Single step tableaux for modal logics. Computational properties, complexity and methodology
• Free-variable semantic tableaux for the logic of fuzzy inequalities
• Modal definability of first-order formulas with free variables and query answering
• A general tableau method for propositional interval temporal logics: theory and implementation
• Free-variable tableaux for monotonic preorders
• 2005 Annual Conference of the Australasian Association for Logic
• scientific article; zbMATH DE number 1189105 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• Free variable tableaux for propositional modal logics
• Certification of prefixed tableau proofs for modal logic
• A general proof certification framework for modal logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• Tableau metatheory for syllogistic logics
• Ground and free-variable tableaux for variants of quantified modal logics
• Refined tableau systems for some modal logics of confluence
• Liberalized variable splitting

Describes a project that uses

Uses Software

• SETHEO
• leanTAP
• ModLeanTAP

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 Q5955622)