Terminating modal tableaux with simple completeness proof

MaRDI QIDQ3509052zbMATH OpenFDO

Authors Olivier Gasquet, Andreas Herzig, Mohamad Sahade

Publication date 1 July 2008

zbMATH Keywords

automatic proofmodal logicstableau methods

Mathematics Subject Classification ID

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

Recommendations

• Modal tableaux: completeness vs. termination
• TABLEAUX: A general theorem prover for modal logics
• scientific article; zbMATH DE number 1267561
• A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments
• Strongly analytic tableaux for normal modal logics

Cited in

(7)

• TABLEAUX: A general theorem prover for modal logics
• LotrecScheme
• Modal tableaux: completeness vs. termination
• Tableau-based reasoning for graph properties
• Terminating tableaux for the basic fragment of simple type theory
• Tableau metatheorem for modal logics
• Intuitionistic modal logics: tips and clips

Describes a project that uses

Uses Software

• LoTREC

This page was built for publication: Terminating modal tableaux with simple completeness proof

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