This project formalizes the construction of uniform interpolants for basic modal logic K, Gödel-Löb provability logic GL, and intuitionistic strong Löb logic iSL. The latter includes the calculation of uniform interpolants for intuitionistic logic IL.
A uniform interpolant calculator is available here:
https://hferee.github.io/UIML/demo.html
The calculator parses an input formula and computes the uniform interpolants for the various logics listed above.
This calculator was built by extracting the relevant Coq functions to OCaml code, which is then further compiled to Javascript.
Compiling the project requires Coq version 8.17.1 and may not compile on other versions. One may enforce this locally by running
opam pin coq 8.19.2 in the project folder.
There is a rudimentary install script install.sh in this folder.
The proof library depends on coq and coq-stdpp.
Building the demo further requires js_of_ocaml and angstrom.
All of the above are available on opam.
The proof library compiles with make.
The documentation builds with make doc.
The documentation generated by coqdoc is available here: https://hferee.github.io/UIML/toc.html