higher-order-logic

There are 20 repositories under higher-order-logic topic.

  • 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 ML63849663143

  • acharal/hopes

    Higher Order Prolog with Extensional Semantics

    Language:Haskell53825

  • leoprover/Leo-III

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

    Language:Scala43185110

  • nyuichi/LeanHOL

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

    Language:Lean21300

  • gilith/opentheory

    The opentheory tool processes higher order logic theory packages

    Language:Standard ML152103

  • gilith/hol

    A purely functional higher order logic kernel

    Language:Haskell11201

  • p-samuel/anonymous-methods

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

    Language:Pascal7200

  • binghe/HOL-CCS

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

    Language:TeX6445

  • leoprover/embed_modal

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

    Language:Python5472

  • andrewppar/logos

    A Proof Assistant for Philosophers

    Language:Clojure4300

  • veracruz-project/supervisionary

    The Supervisionary proof-checking kernel for higher-order logic

    Language:Rust3300

  • mmottl/fun-trans

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

    Language:Vim Script230

  • theoremprover-museum/egal

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

    Language:OCaml2500

  • Sup3Legacy/PyMaths

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

    Language:Python110

  • binghe/HOL-Probability

    Measure, Lebesgue and Probability Theory for HOL4 (leftovers)

    Language:Standard ML0301

  • chrisjpm/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:Haskell0000

  • DominicPM/supervisionary

    Supervisionary: a proof-checking system for HOL

    Language:Rust0200

  • hwixley/AR-Coursework1

    Theorem proving in Isabelle

    Language:Isabelle0100

  • leoprover/ddl2thf

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

    Language:Java0600

  • James-Oswald/Eminence-Prover-concept

    A proof of concept for a theorem prover for DCEC reasoning

    Language:C++11