Supervisionary: a proof-checking system for HOL
-
Updated
May 2, 2023 - Rust
Supervisionary: a proof-checking system for HOL
Modélisation de concepts mathématiques et raisonnements sur ces derniers.
A Proof Assistant for Philosophers
A framework for automated transformation of functional programs (e.g. partial evaluation, common subexpression elimination, etc.) written in LambdaProlog.
Calculus of Communicating Systems (CCS) in Higher Order Logic (HOL4)
super tiny implementation of higher-order logic proof assistant in lean
Using higher-order logic to copy JavaScript's "filter", "map" and "reduce" functions in Delphi.
Theorem proving in Isabelle
DDL2THF -- A preprocessor for translating problems in Dyadic Deontic Logic into THF problems
A proof of concept for a theorem prover for DCEC reasoning
Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory
A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% 🎉
The Supervisionary proof-checking kernel for higher-order logic
A purely functional higher order logic kernel
Measure, Lebesgue and Probability Theory for HOL4 (leftovers)
A tool for translating higher-order modal logic problems into classical higher-order logic
The opentheory tool processes higher order logic theory packages
Higher Order Prolog with Extensional Semantics
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Add a description, image, and links to the higher-order-logic topic page so that developers can more easily learn about it.
To associate your repository with the higher-order-logic topic, visit your repo's landing page and select "manage topics."