Tableau methods of proof for modal logics

DOI10.1305/ndjfl/1093894722zbMath0184.28102OpenAlexW1978260344MaRDI QIDQ2535854

Melvin Fitting

Publication date: 1972

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1305/ndjfl/1093894722

zbMATH Keywords

general logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45)

Related Items

Barcan Both Ways ⋮ Nested sequents for intuitionistic modal logics via structural refinement ⋮ First-order intensional logic ⋮ Labeled sequent calculi for modal logics and implicit contractions ⋮ Prefixed tableaus and nested sequents ⋮ Nested sequents for intermediate logics: the case of Gödel-Dummett logics ⋮ Cut Elimination for Extended Sequent Calculi ⋮ A Tableaux System for Deontic Action Logic ⋮ Unnamed Item ⋮ Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems ⋮ Nested sequents for intuitionistic logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse ⋮ Modal interpolation via nested sequents ⋮ Through an Inference Rule, Darkly ⋮ The complexity of identifying characteristic formulae ⋮ Using tableau to decide description logics with full role negation and identity ⋮ Unnamed Item ⋮ Strongly analytic tableaux for normal modal logics ⋮ Intuitionistic Layered Graph Logic ⋮ Description Logics ⋮ A general proof certification framework for modal logic ⋮ A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas ⋮ Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ Model existence theorems for modal and intuitionistic logics ⋮ Interpolation for first order S5