Formalizing a Seligman-style tableau system for hybrid logic (short paper)

DOI10.1007/978-3-030-51074-9_27MaRDI QIDQ2096470zbMATH OpenOpenAlexFDO

Authors Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_27

zbMATH Keywords

completenesshybrid logicIsabelle/HOLsoundness

Mathematics Subject Classification ID

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

Cites work

• Completeness and termination for a Seligman-style tableau system
• Constructive Formalization of Hybrid Logic with Eventualities
• Formalization of the Resolution Calculus for First-Order Logic
• scientific article; zbMATH DE number 1163391 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Hybrid logic and its proof-theory
• Hybrid logics and ontology languages
• Hybrid logics: Characterization, interpolation and complexity
• Internalization: The case of hybrid logics
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof methods for modal and intuitionistic logics
• Proof theory of a multi-lane spatial logic
• Representation, reasoning, and relational structures: a hybrid logic manifesto
• Soundness and completeness proofs by coinductive methods
• Synthetic completeness proofs for Seligman-style tableau systems
• Termination for Hybrid Tableaus

Cited in

(11)

• Formalized soundness and completeness of epistemic logic
• A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities
• Resolution in modal, description and hybrid logic
• An efficient approach to nominal equalities in hybrid logic tableaux
• A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
• Tableau-based Decision Procedures for Hybrid Logic
• scientific article; zbMATH DE number 1950252 (Why is no real title available?)
• Pragmatic Formal Specification of System Properties by Tables
• Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
• A modular formalization of superposition in Isabelle/HOL
• Synthetic completeness for a terminating Seligman-style tableau system

Describes a project that uses

Uses Software

• Isabelle/HOL
• Archive of Formal Proofs

This page was built for publication: Formalizing a Seligman-style tableau system for hybrid logic (short paper)

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