5 Search Results for "Perini Brogi, Cosimo"

Artifact
Software
DOI: 10.4230/artifacts.25484
HOLMS: A HOL Light Library for Modal Systems

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Abstract
Cite as

Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi. HOLMS: A HOL Light Library for Modal Systems (Software, Source code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25484,
   title = {{HOLMS: A HOL Light Library for Modal Systems}}, 
   author = {Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:36edca29f53f3fdd0a7fc675702990743eda4c8d}{\texttt{swh:1:dir:36edca29f53f3fdd0a7fc675702990743eda4c8d}} (visited on 2026-02-18)},
   url = {https://github.com/HOLMS-lib/HOLMS},
   doi = {10.4230/artifacts.25484},
}
Artifact
Software
DOI: 10.4230/artifacts.25485
Webpage of HOLMS: A HOL Light Library for Modal Systems

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Abstract
Cite as

Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi. Webpage of HOLMS: A HOL Light Library for Modal Systems (Software, Project Documentation Website). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{holms-website,
   title = {{Webpage of HOLMS: A HOL Light Library for Modal Systems}}, 
   author = {Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
   note = {Software (visited on 2026-02-18)},
   url = {https://holms-lib.github.io/},
   doi = {10.4230/artifacts.25485},
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.40
Completeness of First-Order Bi-Intuitionistic Logic

Authors: Dominik Kirst and Ian Shillito

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.
Cite as

Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.CSL.2025.40,
  author =	{Kirst, Dominik and Shillito, Ian},
  title =	{{Completeness of First-Order Bi-Intuitionistic Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.40},
  URN =		{urn:nbn:de:0030-drops-227979},
  doi =		{10.4230/LIPIcs.CSL.2025.40},
  annote =	{Keywords: bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.26
A Formal Proof of Modal Completeness for Provability Logic

Authors: Marco Maggesi and Cosimo Perini Brogi

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation. In particular, we show how we adapted the proof in the Boolos' monograph according to the formal language and tools at hand. The strategy we develop here overcomes the technical difficulty due to the non-compactness of GL, and simplify the implementation. Moreover, it can be applied to other normal modal systems with minimal changes.
Cite as

Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{maggesi_et_al:LIPIcs.ITP.2021.26,
  author =	{Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Formal Proof of Modal Completeness for Provability Logic}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26},
  URN =		{urn:nbn:de:0030-drops-139215},
  doi =		{10.4230/LIPIcs.ITP.2021.26},
  annote =	{Keywords: Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light Theorem Prover}
}
  • Refine by Type
  • 3 Document/PDF
  • 2 Artifact
  • 2 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 1 2025
  • 1 2021

  • Refine by Author
  • 4 Maggesi, Marco
  • 4 Perini Brogi, Cosimo
  • 3 Bilotta, Antonella
  • 1 Kirst, Dominik
  • 1 Shillito, Ian

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Higher order logic
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 3 HOL Light
  • 2 Automated Reasoning
  • 2 Modal Logic
  • 2 Proof Assistants
  • 2 Theorem Proving
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact