g4ip: A theorem prover for propositional logic that uses G4ip

[ library, logic, mit ] [ Propose Tags ]


  • G4ip
    • G4ip.Decider
    • G4ip.Proposition


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS]
Dependencies base (>=4.6 && <4.7) [details]
License MIT
Author Josh Acay
Maintainer coskuacay@gmail.com
Category Logic
Home page https://github.com/cacay/G4ip
Uploaded by cacay at 2017-03-20T22:01:29Z
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 961 total (5 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2017-03-20 [all 3 reports]

Readme for g4ip-

[back to package description]


Implementation of a theorem prover for propositional logic using G4ip in Haskell.

File Structure

  • 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

Testing Manually

  • Startup ghci
  • Load Main.hs by typing :l Main
  • Use decide prop to see if prop 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.