stp: Simple Theorem Prover

[ bsd3, library, math, program ] [ Propose Tags ]

Simple Theorem Prover constructs a proof tree and searches for a target/conclusion given a list of rewrite rules and axioms/theorems.

[Skip to Readme]
Versions [faq],
Change log
Dependencies base (==4.*), containers (==, regex-compat (==0.95.1), stp [details]
License BSD-3-Clause
Copyright (c) 2018 Boro Sitnikovski
Author Boro Sitnikovski
Category Math
Home page
Source repo head: git clone
this: git clone
Uploaded by bor0 at Wed Nov 21 19:11:40 UTC 2018
Distributions NixOS:
Executables mu-test
Downloads 215 total (35 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2018-11-21 [all 1 reports]


[Index] [Quick Jump]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for stp-

[back to package description]

Simple Theorem Prover

Simple Theorem Prover is a proof tree generator. It allows for specifying axioms and inference rules, and then by quering the program it will produce all valid combinations of inference in attempt to reach a target result.

This project is based on Simple theorem prover in Racket.


Make sure you have ghc and cabal installed. Also, make sure that cabal update is ran to ensure latest version of packages is used.


  1. Run cabal sandbox init
  2. Run cabal install to install dependencies and build this project
  3. Run cabal run to run the example

Copyright 2018, Boro Sitnikovski. All rights reserved.