Conference paper · Journal article · Book chapter
Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper) : (Short Paper)
In
Lecture Notes in Computer Science
—
2020, Volume 12166, pp. 474-481
Abstract
Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof.
Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.
| Language: | English |
|---|---|
| Publisher: | Springer |
| Year: | 2020 |
| Pages: | 474-481 |
| Proceedings: | 10th International Joint Conference on Automated Reasoning |
| Series: | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Journal subtitle: | 10th International Joint Conference, Ijcar 2020, Paris, France, July 1–4, 2020, Proceedings, Part I |
| ISBN: | 3030510735 , 3030510743 , 9783030510732 and 9783030510749 |
| ISSN: | 03029743 and 16113349 |
| Types: | Conference paper , Journal article and Book chapter |
| DOI: | 10.1007/978-3-030-51074-9_27 |
| ORCIDs: | From, Asta Halkjær , 0000-0001-9345-552X and Villadsen, Jørgen |
Keywords
