Eminence Prover
A theorem prover for proof-theoretic higher order modal logic
|
:spades: Eminence in shadowing :chess_pawn:
EminenceProver is a high-order modal logic theorem prover, particularly designed for reasoning in the logics DCEC* and IDCEC. On the backend we make use of a garden of other theorem provers which currently include:
We intend to someday also include backends for:
With CMake
We build the docs separately from the CMake build
For Building:
For Docs:
Not currently a dependency but was or may be at some point: