summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcacay <>2017-03-20 22:01:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2017-03-20 22:01:00 (GMT)
commitc6c7ae9d7eb88091917a04638579818897e593be (patch)
tree7cd6dd9b6221f16dcbce710123539a1f99b2308f
version 0.1.0.0HEAD0.1.0.0master
-rw-r--r--G4ip/Decider.hs80
-rw-r--r--G4ip/Proposition.hs71
-rw-r--r--G4ip/TestMain.hs20
-rw-r--r--G4ip/Tester.hs144
-rw-r--r--LICENSE22
-rw-r--r--README.md31
-rw-r--r--Setup.hs2
-rw-r--r--g4ip.cabal40
8 files changed, 410 insertions, 0 deletions
diff --git a/G4ip/Decider.hs b/G4ip/Decider.hs
new file mode 100644
index 0000000..e9a3b4a
--- /dev/null
+++ b/G4ip/Decider.hs
@@ -0,0 +1,80 @@
+{-|
+Module : G4ip.Decider
+Description : Decide if a proposition is provable
+Maintainer : Josh Acay <cacay@cmu.edu>
+Stability : experimental
+-}
+module G4ip.Decider (decide) where
+
+import Control.Arrow (second)
+import Data.List (inits, tails)
+import Data.Tuple (uncurry)
+
+import G4ip.Proposition (Prop (..))
+
+
+-- | Decide if a proposition has a proof
+decide :: Prop -> Bool
+decide = right ([], [])
+
+
+-- (invertible propositions, non-invertible propositions)
+type Context = ([Prop], [Prop])
+
+
+-- Add a proposition to the context
+add :: Prop -> Context -> Context
+add p ctx@(inv, other) = case p of
+ Atom _ -> (inv, p : other) -- Assume not-invertible
+ T -> ctx -- Leave out since useless
+ F -> ([F], []) -- Do not need anything else
+ And _ _ -> (p : inv, other)
+ Or _ _ -> (p : inv, other)
+ Imp (Atom _) _ -> (inv, p : other)
+ Imp (Imp _ _) _ -> (inv, p : other)
+ Imp _ _ -> (p : inv, other)
+
+
+-- Invertible decisions
+right :: Context -> Prop -> Bool
+right _ T = True
+right ctx (And a b) = right ctx a && right ctx b
+right ctx (Imp a b) = right (add a ctx) b
+right (And a b : inv, other) c = right (add a $ add b (inv, other)) c
+right (F : _, _) _ = True
+right (Or a b : inv, other) c =
+ right (add a (inv, other)) c && right (add b (inv, other)) c
+right (Imp T b : inv, other) c = right (add b (inv, other)) c
+right (Imp F _ : inv, other) c = right (inv, other) c
+right (Imp (And d e) b : inv, other) c =
+ right (add (Imp d $ Imp e b) (inv, other)) c
+right (Imp (Or d e) b : inv, other) c =
+ right (add (Imp e b) $ add (Imp d b) (inv, other)) c
+right ([], other) p@(Or a b) =
+ left other p || right ([], other) a || right ([], other) b
+right ([], other) c = left other c
+
+
+-- Non-invertible decisions. The invertible assumptions should be empty.
+left :: [Prop] -> Prop -> Bool
+left other c = any (`elim` c) (pulls other)
+
+
+-- Reduce one non-invertible assumption and continue proof
+elim :: (Prop, [Prop]) -> Prop -> Bool
+elim (Atom s1, _) (Atom s2) = s1 == s2
+elim (Atom s, _) _ = False
+elim (Imp (Atom s) b, other) c =
+ right ([], other) (Atom s) && right (add b ([], other)) c
+elim (Imp (Imp d e) b, other) c =
+ right (add d $ add (Imp e b) ([], other)) e && right (add b ([], other)) c
+
+
+-- | Pull one element out for all elements. For example,
+--
+-- > pulls "abc" == [('a',"bc"),('b',"ac"),('c',"ab")]
+pulls :: [a] -> [(a, [a])]
+pulls xs = take (length xs) $ zipWith (second . (++)) (inits xs) breakdown
+ where pull (x : xs) = (x, xs)
+ breakdown = map pull (tails xs)
+
diff --git a/G4ip/Proposition.hs b/G4ip/Proposition.hs
new file mode 100644
index 0000000..bd2d122
--- /dev/null
+++ b/G4ip/Proposition.hs
@@ -0,0 +1,71 @@
+{-|
+Module : G4ip.Proposition
+Description : Representation of propositions
+Maintainer : Josh Acay <cacay@cmu.edu>
+Stability : experimental
+-}
+module G4ip.Proposition (
+ Prop (..)
+ , (/\)
+ , (\/)
+ , (==>)
+ , (<==)
+ , (<=>)
+ , neg) where
+
+
+data Prop = Atom String
+ | T
+ | F
+ | And Prop Prop
+ | Or Prop Prop
+ | Imp Prop Prop
+ deriving (Eq, Ord)
+
+
+infixr 3 /\
+infixr 2 \/
+infixr 1 ==>
+infixr 1 <==
+infixr 0 <=>
+
+
+(/\) :: Prop -> Prop -> Prop
+(/\) = And
+
+
+(\/) :: Prop -> Prop -> Prop
+(\/) = Or
+
+
+(==>) :: Prop -> Prop -> Prop
+(==>) = Imp
+
+
+(<==) :: Prop -> Prop -> Prop
+(<==) = flip Imp
+
+
+(<=>) :: Prop -> Prop -> Prop
+a <=> b = And (Imp a b) (Imp b a)
+
+
+neg :: Prop -> Prop
+neg a = a ==> F
+
+
+instance Show Prop where
+ show = showImp
+ where
+ showImp (Imp a b) = showAndOr a ++ " ==> " ++ showAndOr b
+ showImp p = showAndOr p
+
+ showAndOr (And a b) = showAtom a ++ " /\\ " ++ showAtom b
+ showAndOr (Or a b) = showAtom a ++ " \\/ " ++ showAtom b
+ showAndOr p = showAtom p
+
+ showAtom (Atom s) = s
+ showAtom T = "T"
+ showAtom F = "F"
+ showAtom p = "(" ++ showImp p ++ ")"
+
diff --git a/G4ip/TestMain.hs b/G4ip/TestMain.hs
new file mode 100644
index 0000000..ffc43b0
--- /dev/null
+++ b/G4ip/TestMain.hs
@@ -0,0 +1,20 @@
+{-|
+Module : Main
+Description : Run the default test suite
+Maintainer : Josh Acay <cacay@cmu.edu>
+Stability : experimental
+-}
+module Main where
+
+import Control.Monad (void, when)
+import System.Exit (exitFailure)
+
+import G4ip.Decider (decide)
+import G4ip.Tester (tests, runTests)
+
+
+main :: IO ()
+main = do
+ errorCount <- runTests tests
+ when (errorCount > 0)
+ exitFailure
diff --git a/G4ip/Tester.hs b/G4ip/Tester.hs
new file mode 100644
index 0000000..fe6dd92
--- /dev/null
+++ b/G4ip/Tester.hs
@@ -0,0 +1,144 @@
+{-|
+Module : G4ip.Tester
+Description : Testing module for 'decide'
+Maintainer : Josh Acay <cacay@cmu.edu>
+Stability : experimental
+-}
+module G4ip.Tester (Test, tests, check, runTests) where
+
+import Control.Monad
+import Data.Tuple (uncurry)
+
+import G4ip.Decider (decide)
+import G4ip.Proposition (Prop (Atom, T, F), (/\), (\/), (==>), (<==), (<=>), neg)
+
+
+-- | A test is a proposition paired with whether or not it is provable
+type Test = (Prop, Bool)
+
+
+-- Some shortcuts
+a = Atom "A"
+b = Atom "B"
+c = Atom "C"
+d = Atom "D"
+e = Atom "E"
+f = Atom "F"
+p = Atom "P"
+s = Atom "S"
+k = Atom "K"
+l = Atom "L"
+
+
+-- * Put tests here
+
+tests = [
+ {- I -} ( a ==> a , True ),
+ {- K -} ( a ==> (b ==> a) , True ),
+ {- S -} ( (a ==> b) ==> (a ==> (b ==> c)) ==> (a ==> c) , True ),
+
+ {- Peirce's law -- not provable, generally -}
+ ( ((a ==> b) ==> a) ==> a , False ),
+ {- ... but by Glivenko's theorem, its double-negation should be! -}
+ ( neg (neg (((a ==> b) ==> a) ==> a)) , True ),
+
+ {- andComm: -}
+ ( a /\ b ==> b /\ a , True ),
+ {- hw01, orComm: -}
+ ( a \/ b ==> b \/ a , True ),
+
+ {- hw01, clue: -}
+ ( (p ==> (c /\ k) \/ (d /\ l))
+ ==> (neg k ==> s)
+ ==> (d \/ l)
+ ==> (p ==> neg s) /\ (s ==> neg p)
+ ==> (c ==> neg d) /\ (d ==> neg c)
+ ==> (k ==> neg l) /\ (l ==> neg k)
+ ==> neg p , True ),
+
+ {- hw02, implOr: -}
+ ( (a \/ c) /\ (b ==> c) ==> (a ==> b) ==> c, True ),
+
+ {- some basic propositional (non-)tautologies -}
+ ( (a ==> b ==> c) <=> (a /\ b ==> c) , True ),
+ ( (a ==> b /\ c) <=> (a ==> b) /\ (a ==> c) , True ),
+ ( (a ==> b \/ c) ==> (a ==> b) \/ (a ==> c) , False ),
+ ( (a ==> b \/ c) <== (a ==> b) \/ (a ==> c) , True ),
+ ( ((a ==> b) ==> c) ==> ((a \/ b) /\ (b ==> c)) , False ),
+ ( ((a ==> b) ==> c) <== ((a \/ b) /\ (b ==> c)) , True ),
+ ( (a \/ b ==> c) <=> (a ==> c) /\ (b ==> c) , True ),
+ ( (a /\ (b \/ c)) <=> (a /\ b) \/ (a /\ c) , True ),
+ ( (a \/ (b /\ c)) <=> (a \/ b) /\ (a \/ c) , True ),
+
+ {- some deMorgan-like dualities -}
+ ( neg (a /\ b) ==> neg a \/ neg b , False ),
+ ( neg (a /\ b) <== neg a \/ neg b , True ),
+ ( neg (a \/ b) <=> neg a /\ neg b , True ),
+ ( neg (a ==> b) ==> a /\ neg b , False ),
+ ( neg (a ==> b) <== a /\ neg b , True ),
+ ( neg (neg a) ==> a , False ),
+ ( neg (neg a) <== a , True ),
+ ( neg T <=> F , True ),
+ ( neg F <=> T , True ),
+
+ {- triple-negation elimination -}
+ ( neg (neg (neg a)) <=> neg a , True ),
+ {- three-way transitivity -}
+ ( (a ==> b) ==> (b ==> c) ==> (c ==> d) ==> (a ==> d) , True ),
+
+ {- some test cases for various common mistakes -}
+
+ ( (a ==> b) ==> (a ==> c) ==> a ==> b , True ),
+ ( (a ==> b) ==> (a ==> c) ==> a ==> c , True ),
+ ( a ==> (a ==> b) ==> (a ==> c) ==> b , True ),
+ ( a ==> (a ==> b) ==> (a ==> c) ==> c , True ),
+
+ ( (a ==> b ==> c) ==> a ==> b ==> c , True ),
+ ( (a ==> b ==> c) ==> b ==> a ==> c , True ),
+ ( a ==> b ==> (a ==> b ==> c) ==> c , True ),
+ ( b ==> a ==> (a ==> b ==> c) ==> c , True ),
+
+ {- it turns out that heavily left-nested instances of the identity
+ theorem make really great stress-tests for correctness! -}
+ ( (a ==> b) ==> a ==> b , True ),
+ ( ((a ==> b) ==> c) ==> ((a ==> b) ==> c) , True ),
+ ( (((a ==> b) ==> c) ==> d) ==> (((a ==> b) ==> c) ==> d) , True ),
+ ( ((((a ==> b) ==> c) ==> d) ==> e) ==> (((a ==> b) ==> c) ==> d) ==> e , True ),
+ ( (((((a ==> b) ==> c) ==> d) ==> e) ==> f) ==> ((((a ==> b) ==> c) ==> d) ==> e) ==> f , True ),
+ ( (((((a ==> b) ==> c) ==> d) ==> e) ==> f) ==> (((((a ==> b) ==> c) ==> d) ==> e) ==> f) \/ (((((a ==> b) ==> c) ==> d) ==> e) ==> f) , True ),
+
+ ( ((a ==> b) ==> c) ==> d ==> d \/ d, True )
+ ]
+
+
+-- * Printing
+
+-- | Result is 'True' if the test passes 'False' otherwise
+check :: Prop -> Bool -> IO Bool
+check p expected = do
+ putStr $ "Checking " ++ show p ++ " " ++ expectation ++ "..."
+ putStrLn (if correct then ok else wrong)
+ return correct
+ where
+ expectation = if expected then "provable" else "unprovable"
+ correct = decide p == expected
+
+ ok :: String
+ ok = "\027[1;30m[\027[32m OK! \027[30m]\027[m"
+
+ wrong :: String
+ wrong = "\027[1;30m[\027[31m WRONG \027[30m]\027[m"
+
+
+-- | Run the given tests and report the number of errors
+runTests :: [Test] -> IO Int
+runTests tests = do
+ results <- mapM (uncurry check) tests
+ let errors = sum $ map (fromEnum . not) results
+ putStrLn $ if errors == 0
+ then "*** All tests passed!"
+ else "*** Failed " ++ show errors ++ " out of " ++
+ show (length tests) ++ " tests."
+ return errors
+
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..b0dc947
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,22 @@
+The MIT License (MIT)
+
+Copyright (c) 2015 Josh Acay
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..e462690
--- /dev/null
+++ b/README.md
@@ -0,0 +1,31 @@
+# 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 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).
+
+
+## Contact
+
+Email me at coskuacay@gmail.com for any questions.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/g4ip.cabal b/g4ip.cabal
new file mode 100644
index 0000000..94155c8
--- /dev/null
+++ b/g4ip.cabal
@@ -0,0 +1,40 @@
+name: g4ip
+version: 0.1.0.0
+category: Logic
+synopsis: A theorem prover for propositional logic that uses G4ip
+homepage: https://github.com/cacay/G4ip
+
+license: MIT
+license-file: LICENSE
+
+author: Josh Acay
+maintainer: coskuacay@gmail.com
+
+build-type: Simple
+cabal-version: >=1.10
+
+extra-source-files: README.md
+
+
+library
+
+ default-language: Haskell98
+
+ exposed-modules: G4ip.Decider
+ G4ip.Proposition
+
+ build-depends: base >= 4.6 && < 4.7
+
+
+test-suite test-g4ip
+
+ default-language: Haskell98
+
+ type: exitcode-stdio-1.0
+ main-is: G4ip/TestMain.hs
+
+ build-depends: base >= 4.6 && < 4.7,
+ g4ip
+
+ other-modules: G4ip.Tester
+