Proper

Propositional logic theorem prover in Haskell

Proper is also available as a hackage. The Hackage contains a library for propositional logic as well as executables for parsing and checking theorems in propositional logic. See the example files in the top level directory for details.

Installation

At the command line:

bash-3.2$ git clone https://github.com/dillonhuff/Proper.git
Cloning into 'Proper'...
remote: Counting objects: 317, done.        
remote: Total 317 (delta 0), reused 0 (delta 0), pack-reused 317        
Receiving objects: 100% (317/317), 40.66 KiB | 0 bytes/s, done.
Resolving deltas: 100% (161/161), done.
Checking connectivity... done.
bash-3.2$ cd Proper/
bash-3.2$ ls
DemorganThm.txt		ExampleTheoremFile.txt	LICENSE			README.md		src
EmptyThm.txt		FalseThm.txt		Proper.cabal		Setup.hs		test
bash-3.2$ cabal install
Warning: The package list for 'hackage.haskell.org' is 158.7 days old.
Run 'cabal update' to get the latest list of available packages.
Resolving dependencies...
Configuring Proper-0.5.2.2...
Building Proper-0.5.2.2...
Installed Proper-0.5.2.2
Updating documentation index
/Users/dillon/Library/Haskell/share/doc/x86_64-osx-ghc-7.10.3/index.html
bash-3.2$ ls
DemorganThm.txt		ExampleTheoremFile.txt	LICENSE			README.md		dist			test
EmptyThm.txt		FalseThm.txt		Proper.cabal		Setup.hs		src
bash-3.2$ ./dist/build/Proper-tests/Proper-tests
Cases: 11  Tried: 11  Errors: 0  Failures: 0
Cases: 9  Tried: 9  Errors: 0  Failures: 0
Cases: 14  Tried: 14  Errors: 0  Failures: 0
Cases: 7  Tried: 7  Errors: 0  Failures: 0
Cases: 3  Tried: 3  Errors: 0  Failures: 0
Cases: 8  Tried: 8  Errors: 0  Failures: 0
Cases: 12  Tried: 12  Errors: 0  Failures: 0
Cases: 4  Tried: 4  Errors: 0  Failures: 0
Cases: 4  Tried: 4  Errors: 0  Failures: 0
bash-3.2$ ./dist/build/Proper/Proper FalseThm.txt 
THEOREM
("a" <-> "b")
(~("c") | (~("d") & "a"))

|=

("a" | "b")

is False
bash-3.2$ ./dist/build/Proper/Proper DemorganThm.txt 
THEOREM
("a" <-> "f")
(~("c") -> ("a" & "l"))
~(~(~("c")))

|=

(~(("l" | ~("f"))) <-> (~("l") & "f"))

is True

Using Proper as a library from within a Haskell program

After installing Proper, use put the following code in Main.hs:

import Proper.Formula

main :: IO ()
main =
  let a = val "a"
      thm = theorem [neg $ neg a] a in
   do
     putStrLn $ show thm
     putStrLn $ "is true ? " ++ (show $ checkTheorem thm)

This code should print out:

bash-3.2$ ghci
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
Prelude> :l Main.hs
[1 of 1] Compiling Main             ( Main.hs, interpreted )
Ok, modules loaded: Main.
*Main> main
THEOREM
~(~("a"))

|=

"a"
is true ? True