HOLMS: A HOL Light Library for Modal Systems

Bilotta, Antonella; Maggesi, Marco; Perini Brogi, Cosimo

doi:10.4230/artifacts.25484

Artifact

HOLMS: A HOL Light Library for Modal Systems Software

Authors Antonella Bilotta , Marco Maggesi , Cosimo Perini Brogi

Part of: Collection: Supplementary Materials
License: BSD 2-Clause "Simplified" License
Publication Date: 2026-02-18

Document Identifiers

DOI: 10.4230/artifacts.25484
URN: urn:nbn:de:0030-drops-254847

Author Details

Antonella Bilotta

Scuola Normale Superiore di Pisa, Italy

Marco Maggesi

University of Florence, Italy

Cosimo Perini Brogi

IMT School for Advanced Studies Lucca, Italy

Content

Software (Source code): https://github.com/HOLMS-lib/HOLMS
archived version

Version/Status

Content created at: 2024-09-26
Status: Active (at the time of publication 2026-02-18)

Cite As Get BibTex

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) https://doi.org/10.4230/artifacts.25484

Description

This repository contains HOLMS (HOL-Light Library for Modal Systems), a modular framework designed to implement modal reasoning within the HOL Light proof assistant.

Subject Classification

Keywords

Theorem Proving
Modal Logic
Proof Assistants
Automated Reasoning
HOL Light

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata

0

Downloads

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail