Completeness of First-Order Bi-intuitionistic Logic

This project formalises the completeness of first-order bi-intuitionistic logic relative to constant domain Kripke semantics.

Building

Compiling the project requires Coq version 8.19.2 and may not compile on other versions. One may enforce this locally by running opam pin coq 8.19.2 in the project folder.

Instruction

The proof library compiles with make all. The documentation builds with make doc.