jack-pappas/NHol

An implementation of higher-order logic (HOL) in F#. Based on hol-light, Isabelle, and HOL4.

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

• Jack Pappas
• Eric Taucher
• Anh-Dung Phan
• Domenico Masini

License

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

Personal Notes

• [Eric's Notes] (https://github.com/jack-pappas/NHol/wiki/Eric's-Notes-Page-1)