simple-resolution-prover

Building

To compile

ghc Main.lhs

... will automatically make dependencies etc

OR you can use "ghci" on parts of this, eg

ghci Main.lhs

Code has been tested with GHC 7.4.1, but doesn't use anything unusual so should work with most versions

Running

Run the executable, or run "main" in ghci

By default, it runs the prover on the theorem in file "eg_two"

Reading the code

Help yourselves! Feel free to raise questions in issues etc.