GitHub topics: higher-order-logic
HOL-Theorem-Prover/HOL
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.
Language: Standard ML - Size: 117 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 661 - Forks: 148
leoprover/Leo-III
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Language: Scala - Size: 34 MB - Last synced at: 5 days ago - Pushed at: 10 days ago - Stars: 46 - Forks: 10
pqnelson/make-a-hol
Grab a shovel, we're making a HOL
Language: Standard ML - Size: 78.1 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 0 - Forks: 0
DominicPM/supervisionary
Supervisionary: a proof-checking system for HOL
Language: Rust - Size: 4.84 MB - Last synced at: 6 days ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0
binghe/HOL-Probability
Measure, Lebesgue and Probability Theory for HOL4 (leftovers)
Language: Standard ML - Size: 3.45 MB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 0 - Forks: 1
HOLMS-lib/HOLMS
HOL-Light Library for Modal Systems
Language: OCaml - Size: 212 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0
mmottl/fun-trans
A framework for automated transformation of functional programs (e.g. partial evaluation, common subexpression elimination, etc.) written in LambdaProlog.
Language: Vim Script - Size: 69.3 KB - Last synced at: 3 months ago - Pushed at: 4 months ago - Stars: 2 - Forks: 0
HOLMS-lib/holms-lib.github.io
HOL Light Library for Modal Systems
Size: 96.7 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0
p-samuel/anonymous-methods
Using higher-order logic to copy JavaScript's "filter", "map" and "reduce" functions in Delphi.
Language: Pascal - Size: 64.5 KB - Last synced at: 2 days ago - Pushed at: 5 months ago - Stars: 7 - Forks: 0
nyuichi/LeanHOL
super tiny implementation of higher-order logic proof assistant in lean
Language: Lean - Size: 21.5 KB - Last synced at: about 2 months ago - Pushed at: over 5 years ago - Stars: 21 - Forks: 0
James-Oswald/Eminence-Prover-concept
A proof of concept for a theorem prover for DCEC reasoning
Language: C++ - Size: 515 KB - Last synced at: 1 day ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
theoremprover-museum/egal
Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory
Language: OCaml - Size: 1.32 MB - Last synced at: about 1 year ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 0
gilith/opentheory
The opentheory tool processes higher order logic theory packages
Language: Standard ML - Size: 53.7 MB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 14 - Forks: 3
binghe/HOL-CCS
Calculus of Communicating Systems (CCS) in Higher Order Logic (HOL4)
Language: TeX - Size: 12.3 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 6 - Forks: 0
hwixley/AR-Coursework1
Theorem proving in Isabelle
Language: Isabelle - Size: 587 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 0 - Forks: 0
leoprover/ddl2thf 📦
DDL2THF -- A preprocessor for translating problems in Dyadic Deontic Logic into THF problems
Language: Java - Size: 325 KB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0
chrisjpm/holbert Fork of liamoc/holbert
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% :tada:
Language: Haskell - Size: 13.3 MB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0
acharal/hopes
Higher Order Prolog with Extensional Semantics
Language: Haskell - Size: 3.48 MB - Last synced at: almost 2 years ago - Pushed at: almost 5 years ago - Stars: 46 - Forks: 6
andrewppar/logos
A Proof Assistant for Philosophers
Language: Clojure - Size: 737 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 4 - Forks: 0
veracruz-project/supervisionary
The Supervisionary proof-checking kernel for higher-order logic
Language: Rust - Size: 827 KB - Last synced at: 10 months ago - Pushed at: about 3 years ago - Stars: 3 - Forks: 0
leoprover/embed_modal
A tool for translating higher-order modal logic problems into classical higher-order logic
Language: Python - Size: 1.54 MB - Last synced at: 8 days ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 2
cs-t1/PyMaths
Modélisation de concepts mathématiques et raisonnements sur ces derniers.
Language: Python - Size: 5.86 KB - Last synced at: 3 months ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 0
gilith/hol
A purely functional higher order logic kernel
Language: Haskell - Size: 118 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 11 - Forks: 1