An implementation of higher-order logic (HOL) in F#. Based on hol-light, Isabelle, and HOL4.
F# Shell
Permalink
Failed to load latest commit information.
.nuget
Common
NHol.Tests
NHol
PredicateCalculus
Tutorial
_docs
packages
.gitattributes
.gitignore
CONTRIBUTING.rst
LICENSE.txt
NHol.bat
NHol.lnk
NHol.sln
NHol.v10.sln
README.md
hol.sh

README.md

NHol

An implementation of higher-order logic (HOL) in F#.

====

Purpose

The project aims at developing a high-order theorem prover in F#. The goal is to leverage the power of functional programming language F# and .NET platform in an interesting context, automated deduction. At the first step, we would like to bring the core features of Hol-light to F#.

Core Team

License

This project is available under Apache 2.0 license. For more information see the License file.

Personal Notes