Implementation of a theorem prover for propositional logic using G4ip in Haskell.
- G4ip/Proposition.hs -- Definition of propositions and some syntactic sugar
- G4ip/Decider.hs -- The actual theorem prover (decider?)
- G4ip/Tester.hs -- For defining and running tests
- G4ip/TestMain.hs -- Actually runs the default test suite
- Startup
ghci
- Load
Main.hs
by typing:l Main
- Use
decide prop
to see ifprop
is provable.
You can use T
, F
, /\
, \/
, ==>
, <==
, <=>
, neg
, and ()
with their usual meanings to form propositions. To form an atom, either use Atom "name"
or use one of the predefined atoms: a
, b
, c
, d
, e
, or f
. Here is an example:
decide $ (neg b ==> neg a) ==> (a ==> b) \/ (a \/ a ==> a)
which prints True
as expected ($
if for associativity, you can use parenthesis if you want).
Email me at coskuacay@gmail.com for any questions.