This project formalises a generalised Hilbert calculus and an interior preorder semantics for the intuitionistic modal logic iS4.
Compiling the project requires Coq version 8.18.0 and may not compile on other versions. One may enforce this locally by running
opam pin coq 8.18.0 in the project folder.
The proof library compiles with make all.
The documentation builds with make doc.
The documentation generated by coqdoc is available here: https://ianshil.github.io/iS4/toc.html