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

DOI10.1007/978-3-030-51074-9_27OpenAlexW3013165824MaRDI QIDQ2096470

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

Publication date: 9 November 2022

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

zbMATH Keywords

completenesshybrid logicsoundnessIsabelle/HOL

Mathematics Subject Classification ID

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

Related Items (1)

Formalized soundness and completeness of epistemic logic

Uses Software

• Isabelle/HOL
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof methods for modal and intuitionistic logics
• Isabelle/HOL. A proof assistant for higher-order logic
• Soundness and completeness proofs by coinductive methods
• Hybrid logics: characterization, interpolation and complexity
• Internalization: The Case of Hybrid Logics
• Formalization of the Resolution Calculus for First-Order Logic
• Hybrid Logics and Ontology Languages
• Completeness and termination for a Seligman-style tableau system
• Constructive Formalization of Hybrid Logic with Eventualities
• Representation, reasoning, and relational structures: a hybrid logic manifesto
• Termination for Hybrid Tableaus
• Proof Theory of a Multi-Lane Spatial Logic
• Hybrid logic and its proof-theory

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