hol: Higher order logic

[ library, logic, mit, program ] [ Propose Tags ]

This package implements a higher order logic kernel with OpenTheory support.

[Skip to Readme]

Downloads

hol-1.3.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

JoeHurd

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	1.0, 1.1, 1.2, 1.3, 1.4
Dependencies	base (>=4.0 && <5.0), bytestring (>=0.9), containers (>=0.5), filepath (>=1.3), parsec (>=3.1), pretty (>=1.1), process (>=1.2), text (>=0.11), transformers (>=0.3) [details]
License	MIT
Author	Joe Leslie-Hurd <joe@gilith.com>
Maintainer	Joe Leslie-Hurd <joe@gilith.com>
Category	Logic
Source repo	head: git clone git://github.com/gilith/hol.git
Uploaded	by JoeHurd at 2017-11-04T15:13:57Z
Distributions	NixOS:1.4
Reverse Dependencies	1 direct, 0 indirect [details]
Executables	hol-pkg
Downloads	2679 total (15 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs available [build log] Last success reported on 2017-11-04 [all 1 reports]

Readme for hol-1.3

[back to package description]

The hol package

The hol package is a Haskell library that implements a higher order logic kernel. It can read proof files in OpenTheory format, and includes a pretty-printer compatible with the standard theory library.

This software is released under the MIT License.

Install

Installing the hol package requires cabal:

git clone https://github.com/gilith/hol.git
cd hol
cabal install

Test

Use cabal to run the test suite:

cabal test

Run

The hol package contains an executable called hol-pkg, which is run as follows:

Usage: hol-pkg INPUT
where INPUT is one of the following forms:
  FILE.art     : a proof article file
  FILE.thy     : a theory package file
  NAME-VERSION : a specific version of an installed theory package
  NAME ...     : the latest installed version of a list of packages

The hol-pkg program reads the INPUT to generate a set of theorems, which are pretty-printed to standard output together with the symbols they contain. For example,

hol-pkg unit

reads the latest installed version of the unit theory package to generate a set of 5 theorems, resulting in the following output:

3 type operators: (->) bool unit
6 constants: (=) (!) (==>) (?) (?!) ()
5 theorems:
  |- !v. v = ()
  |- !f g. f = g
  |- !e. ?fn. fn () = e
  |- !e. ?!fn. fn () = e
  |- !p. p () ==> !x. p x

Profile

Before starting, make sure the GHC system and the GHC text, transformers and parsec libraries are installed with profiling support. On a Debian system the following command installs them:

 apt-get install ghc-prof libghc-text-prof libghc-transformers-prof libghc-parsec3-prof

Next use cabal to install the other dependent libraries with profiling support:

cabal sandbox init
cabal configure --enable-library-profiling --enable-profiling --enable-benchmarks
cabal install --only-dependencies --enable-library-profiling

Build the hol package library and benchmark program:

cabal configure --enable-library-profiling --enable-profiling --enable-benchmarks
cabal build

Use the opentheory tool to create a benchmark file:

 opentheory info --article -o base.art base

Then use cabal to run the benchmark:

cabal bench

The time and memory allocation profile of the program can be viewed in text format:

less hol-profile.prof

Alternatively the memory allocation profile can be viewed as a graph:

hp2ps -e8in -c hol-profile.hp
ps2pdf hol-profile.ps
xpdf hol-profile.pdf