Simple Theorem Prover.

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

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.

Prerequisites

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

Installation

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.