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.

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics

Higher Order Prolog with Extensional Semantics

The opentheory tool processes higher order logic theory packages

A tool for translating higher-order modal logic problems into classical higher-order logic

Measure, Lebesgue and Probability Theory for HOL4 (leftovers)

A purely functional higher order logic kernel

A Proof Assistant for Philosophers

Supervisionary: a proof-checking system for HOL

Calculus of Communicating Systems (CCS) in Higher Order Logic (HOL4)

A framework for automated transformation of functional programs (e.g. partial evaluation, common subexpression elimination, etc.) written in LambdaProlog.

Using higher-order logic to copy JavaScript's "filter", "map" and "reduce" functions in Delphi.

Modélisation de concepts mathématiques et raisonnements sur ces derniers.

HOL-Light Library for Modal Systems

super tiny implementation of higher-order logic proof assistant in lean

HOL Light Library for Modal Systems

DDL2THF -- A preprocessor for translating problems in Dyadic Deontic Logic into THF problems

Theorem proving in Isabelle

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

A proof of concept for a theorem prover for DCEC reasoning