Isabelle's Pure logic, directly extended to FOL/HOL
-
Updated
May 19, 2019 - Isabelle
Isabelle's Pure logic, directly extended to FOL/HOL
Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
Equivalence of natural deduction and sequent calculus in HOL4
A purely functional higher order logic kernel
Coq version of (part of) the HOL-IMP theories accompanying the book "Concrete Semantics with Isabelle/HOL". Formalized using a now outdated version of CoqHammer.
[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
Scripts for deploying HOL Light with Docker (and optional checkpointing)
The opentheory tool processes higher order logic theory packages
Model finder for higher-order logic
Verilog development and verification project for HOL4
Add a description, image, and links to the hol topic page so that developers can more easily learn about it.
To associate your repository with the hol topic, visit your repo's landing page and select "manage topics."