@hackage g4ip0.1.0.0
A theorem prover for propositional logic that uses G4ip
Categories
License
MIT
Maintainer
coskuacay@gmail.com
Links
- Homepage
- Documentation
- No source repository
- Security
Versions
- 0.1.0.0 Mon, 20 Mar 2017
Installation
Dependencies (1)
Dependents (1)
@hackage/acme-everything
G4ip
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 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).
Contact
Email me at coskuacay@gmail.com for any questions.