logic-classes 0.47 → 0.48
raw patch · 5 files changed
+1643/−1 lines, 5 files
Files
- Test/Chiou0.hs +106/−0
- Test/Data.hs +1077/−0
- Test/Logic.hs +436/−0
- Test/TPTP.hs +22/−0
- logic-classes.cabal +2/−1
+ Test/Chiou0.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE OverloadedStrings, StandaloneDeriving #-}+{-# OPTIONS -fno-warn-orphans #-}++module Test.Chiou0 where++import Control.Monad.Identity (runIdentity)+import Control.Monad.Trans (MonadIO, liftIO)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Pred (pApp)+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.KnowledgeBase (ProverT, runProver', Proof(..), ProofResult(..), loadKB, theoremKB {-, askKB, showKB-})+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')+import Data.Logic.Normal.Skolem (NormalT, runNormal)+import Data.Logic.Resolution (SetOfSupport)+import Data.Logic.Test (V(..), Pr(..), AtomicFunction(..), TFormula, TTerm)+import Data.Logic.Types.FirstOrder (Formula, PTerm)+import Data.Map (fromList)+import qualified Data.Set as S+import Data.String (IsString(..))+import Test.HUnit++tests :: Test+tests = TestLabel "Chiou0" $ TestList [loadTest, proofTest1, proofTest2]++loadTest :: Test+loadTest =+ TestCase (assertEqual "Chiuo0 - loadKB test" expected (runProver' Nothing (loadKB sentences)))+ where+ expected :: [Proof TFormula]+ expected = [Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem 1) []])]),+ makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])])]),+ Proof Invalid (S.fromList [makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [var ("x"),var ("y")])]) ([(pApp ("AnimalLover") [var ("x")])])]),+ Proof Invalid (S.fromList [makeINF' ([(pApp ("Animal") [var ("y")]),(pApp ("AnimalLover") [var ("x")]),(pApp ("Kills") [var ("x"),var ("y")])]) ([])]),+ Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])])]),+ Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])])]),+ Proof Invalid (S.fromList [makeINF' ([(pApp ("Cat") [var ("x")])]) ([(pApp ("Animal") [var ("x")])])])]++proofTest1 :: Test+proofTest1 = TestCase (assertEqual "Chiuo0 - proof test 1" proof1 (runProver' Nothing (loadKB sentences >> theoremKB (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula))))++inf' l1 l2 = INF (S.fromList l1) (S.fromList l2)++proof1 :: (Bool, SetOfSupport TFormula V TTerm)+proof1 = (False,+ (S.fromList+ [(makeINF' ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Curiosity") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList [])]))++proofTest2 :: Test+proofTest2 = TestCase (assertEqual "Chiuo0 - proof test 2" proof2 (runProver' Nothing (loadKB sentences >> theoremKB conjecture)))+ where+ conjecture :: TFormula+ conjecture = (pApp "Kills" [fApp "Curiosity" [], fApp (Fn "Tuna") []])++proof2 :: (Bool, SetOfSupport TFormula V TTerm)+proof2 = (True,+ S.fromList+ [(makeINF' ([]) ([]),fromList []),+ (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])++testProof :: MonadIO m => String -> (TFormula, Bool, (S.Set (ImplicativeForm TFormula))) -> ProverT (ImplicativeForm TFormula) (NormalT V TTerm m) ()+testProof label (question, expectedAnswer, expectedProof) =+ theoremKB question >>= \ (actualFlag, actualProof) ->+ let actual' = (actualFlag, S.map fst actualProof) in+ if actual' /= (expectedAnswer, expectedProof)+ then error ("\n Expected:\n " ++ show (expectedAnswer, expectedProof) +++ "\n Actual:\n " ++ show actual')+ else liftIO (putStrLn (label ++ " ok"))++loadCmd :: Monad m => ProverT (ImplicativeForm TFormula) (NormalT V TTerm m) [Proof TFormula]+loadCmd = loadKB sentences++sentences :: [TFormula]+sentences = [exists "x" ((pApp "Dog" [var "x"]) .&. (pApp "Owns" [fApp "Jack" [], var "x"])),+ for_all "x" (((exists "y" (pApp "Dog" [var "y"])) .&. (pApp "Owns" [var "x", var "y"])) .=>. (pApp "AnimalLover" [var "x"])),+ for_all "x" ((pApp "AnimalLover" [var "x"]) .=>. (for_all "y" ((pApp "Animal" [var "y"]) .=>. ((.~.) (pApp "Kills" [var "x", var "y"]))))),+ (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []]) .|. (pApp "Kills" [fApp "Curiosity" [], fApp "Tuna" []]),+ pApp "Cat" [fApp "Tuna" []],+ for_all "x" ((pApp "Cat" [var "x"]) .=>. (pApp "Animal" [var "x"]))]
+ Test/Data.hs view
@@ -0,0 +1,1077 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -fno-warn-name-shadowing -fno-warn-missing-signatures #-}+module Test.Data+ ( tests+ , allFormulas+ , proofs+{-+ , formulas+ , animalKB+ , animalConjectures+ , chang43KB+ , chang43Conjecture+ , chang43ConjectureRenamed+-}+ ) where++import Data.Boolean.SatSolver (Literal(..))+import Data.Generics (Typeable)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), for_all', exists', convertFOF)+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.Classes.Skolem (Skolem(toSkolem))+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Classes.Negatable (Negatable(..))+import qualified Data.Logic.Classes.Literal as N+import qualified Data.Logic.Instances.Chiou as C+import Data.Logic.KnowledgeBase (WithId(WithId, wiItem, wiIdent), Proof(..), ProofResult(..))+import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')+import Data.Logic.Test (TestFormula(..), TestProof(..), Expected(..), ProofExpected(..), doTest, doProof)+import Data.Map (fromList)+import qualified Data.Set as S+import Data.String (IsString)+import Test.HUnit++tests :: (FirstOrderFormula formula term v p f, N.Literal formula term v p f, Eq term, Show term, Show formula, Show v) =>+ [TestFormula formula term v p f] -> [TestProof formula term v] -> Test+tests fs ps =+ TestLabel "New" $ TestList (map doTest fs ++ map doProof ps)++allFormulas :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, Typeable formula, IsString v, IsString p, IsString f) =>+ [TestFormula formula term v p f]+allFormulas = (formulas +++ concatMap snd [animalKB, chang43KB] +++ animalConjectures +++ [chang43Conjecture, chang43ConjectureRenamed])++formulas :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ [TestFormula formula term v p f]+formulas =+ let n = (.~.) :: Logic formula => formula -> formula+ p = pApp "p" :: [term] -> formula+ q = pApp "q" :: [term] -> formula+ r = pApp "r" :: [term] -> formula+ s = pApp "s" :: [term] -> formula+ t = pApp "t" :: [term] -> formula+ p0 = p [] :: formula+ q0 = q [] :: formula+ r0 = r [] :: formula+ s0 = s [] :: formula+ t0 = t [] :: formula+ (x, y, z, u, v, w) :: (term, term, term, term, term, term) =+ (var "x", var "y", var "z", var "u", var "v", var "w") in+ [ + TestFormula+ { formula = p0 .|. q0 .&. r0 .|. n s0 .&. n t0+ , name = "operator precedence"+ , expected = [ FirstOrderFormula ((p0 .|. q0) .&. (r0 .|. (n s0)) .&. (n t0)) ] }+ , TestFormula+ { formula = pApp (fromBool True) []+ , name = "True"+ , expected = [ClauseNormalForm (toSS [[]])] }+ , TestFormula+ { formula = pApp (fromBool False) []+ , name = "False"+ , expected = [ClauseNormalForm (toSS [])] }+ , TestFormula+ { formula = pApp "p" []+ , name = "p"+ , expected = [ClauseNormalForm (toSS [[pApp "p" []]])] }+ , let p = pApp "p" [] in+ TestFormula+ { formula = p .&. ((.~.) (p))+ , name = "p&~p"+ , expected = [ PrenexNormalForm ((pApp ("p") []) .&. (((.~.) (pApp ("p") []))))+ , ClauseNormalForm (toSS [[(p)], [((.~.) (p))]])+ ] }+ , TestFormula+ { formula = pApp "p" [var "x"]+ , name = "p[x]"+ , expected = [ClauseNormalForm (toSS [[pApp "p" [x]]])] }+ , let f = pApp "f"+ q = pApp "q" in+ TestFormula+ { name = "iff"+ , formula = for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))+ , expected = [ PrenexNormalForm + (for_all "x"+ (for_all "y"+ (for_all "z"+ (exists "z2"+ ((q [x,y] .&.+ ((f [z,x] .&. f [z,y]) .|.+ ((((.~.) (f [z,x])) .&. ((.~.) (f [z,y])))))) .|. ((((.~.) (q [x,y])) .&.+ ((((f [var ("z2"),x] .&. (((.~.) (f [var ("z2"),y])))) .|.+ (((.~.) (f [var ("z2"),x])))) .&. f [var ("z2"),y])))))+ ))))+ , ClauseNormalForm ++-- [[((.~.) (q [var "x",var "y"])),+-- ((.~.) (f [var "z",var "x"])),+-- (f [var "z",var "y"])],+-- [((.~.) (q [var "x",var "y"])),+-- ((.~.) (f [var "z",var "y"])),+-- (f [var "z",var "x"])],+-- [(f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"]),+-- (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"]),+-- (q [var "x",var "y"])],+-- [((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"])),+-- (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"]),+-- (q [var "x",var "y"])],+-- [(f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"]),+-- ((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"])),+-- (q [var "x",var "y"])],+-- [((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"])),+-- ((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"])),+-- (q [var "x",var "y"])]]]++ (toSS [[(f [var ("z"),var ("x")]),+ (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+ ((.~.) (f [var ("z"),var ("y")]))],+ [(f [var ("z"),var ("x")]),+ ((.~.) (f [var ("z"),var ("y")])),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))],+ [(f [var ("z"),var ("x")]),+ ((.~.) (f [var ("z"),var ("y")])),+ ((.~.) (q [var ("x"),var ("y")]))],+ [(f [var ("z"),var ("y")]),+ (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+ ((.~.) (f [var ("z"),var ("x")]))],+ [(f [var ("z"),var ("y")]),+ ((.~.) (f [var ("z"),var ("x")])),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))],+ [(f [var ("z"),var ("y")]),+ ((.~.) (f [var ("z"),var ("x")])),+ ((.~.) (q [var ("x"),var ("y")]))],+ [(f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+ (q [var ("x"),var ("y")])],+ [(q [var ("x"),var ("y")]),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+ ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))]])+ ]+ }+ , TestFormula+ { name = "move quantifiers out"+ , formula = (for_all "x" (pApp "p" [x]) .&. (pApp "q" [x]))+ , expected = [PrenexNormalForm (for_all "x2" ((pApp "p" [var ("x2")]) .&. ((pApp "q" [var ("x")]))))]+ }+ , TestFormula+ { name = "skolemize2"+ , formula = exists "x" (for_all "y" (pApp "loves" [x, y]))+ , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem 1) [],y])]+ }+ , TestFormula+ { name = "skolemize3"+ , formula = for_all "y" (exists "x" (pApp "loves" [x, y]))+ , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem 1) [y],y])]+ }+ , TestFormula+ { formula = exists "x" (for_all' ["y", "z"]+ (exists "u"+ (for_all "v"+ (exists "w"+ (pApp "P" [x, y, z, u, v, w])))))+ , name = "chang example 4.1"+ , expected = [ SkolemNormalForm (pApp "P" [fApp (toSkolem 1) [],+ var ("y"),+ var ("z"),+ fApp (toSkolem 2) [var ("y"),var ("z")],+ var ("v"),+ fApp (toSkolem 3) [var ("v"), var ("y"),var ("z")]]) ]+ }+ , TestFormula+ { name = "chang example 4.2"+ -- ∀x ∃y∃z ~P(x,y) & Q(x,z) | R(x,y,z)+ , formula = for_all "x" (exists' ["y", "z"] (((((.~.) (pApp "P" [x, y])) .&. pApp "Q" [x, z]) .|. pApp "R" [x, y, z])))+ -- ∀x ~P(x,Sk1[x]) | R(x,Sk1[x],Sk2[x]) & Q(x,Sk2[x]) | R(x,Sk1[x],Sk2[x])+ , expected = [ SkolemNormalForm+ ((((.~.) (pApp ("P") [var ("x"),var ("y")])) .&.+ ((pApp ("Q") [var ("x"),var ("z")]))) .|.+ ((pApp ("R") [var ("x"),var ("y"),var ("z")])))+ , ClauseNormalForm+ (toSS + [[((.~.) (pApp ("P") [var ("x"),var ("y")])),+ (pApp ("R") [var ("x"),var ("y"),var ("z")])],+ [(pApp ("Q") [var ("x"),var ("z")]),+ (pApp ("R") [var ("x"),var ("y"),var ("z")])]]) ]+ }+ , TestFormula+ { formula = n p0 .|. q0 .&. p0 .|. r0 .&. n q0 .&. n r0+ , name = "chang 7.2.1a - unsat"+ , expected = [ SatSolverSat False ] }+ , TestFormula+ { formula = p0 .|. q0 .|. r0 .&. n p0 .&. n q0 .&. n r0 .|. s0 .&. n s0+ , name = "chang 7.2.1b - unsat"+ , expected = [ SatSolverSat False ] }+ , TestFormula+ { formula = p0 .|. q0 .&. q0 .|. r0 .&. r0 .|. s0 .&. n r0 .|. n p0 .&. n s0 .|. n q0 .&. n q0 .|. n r0+ , name = "chang 7.2.1c - unsat"+ , expected = [ SatSolverSat False ] }+ , let q = pApp "q"+ f = pApp "f"+ sk1 = f [fApp (toSkolem 1) [x,x,y,z],y]+ sk2 = f [fApp (toSkolem 1) [x,x,y,z],x]+ (x, y, z) = (var "x", var "y", var "z") in+ TestFormula+ { name = "distribute bug test"+ , formula = ((((.~.) (q [x,y])) .|.+ ((((.~.) (sk2)) .|. (sk1)) .&.+ (((.~.) (sk1)) .|. (sk2)))) .&.+ ((((sk2) .&.+ ((.~.) (sk1))) .|. ((sk1) .&.+ ((.~.) (sk2)))) .|. (q [x,y])))+ , expected = [ClauseNormalForm+ (toSS+ [[sk2,sk1,pApp ("q") [x,y]],+ [sk2,((.~.) (sk1)),((.~.) (q [x,y]))],+ [sk1,((.~.) (sk2)),((.~.) (q [x,y]))],+ [q [x,y], ((.~.) sk2),((.~.) sk1)]])]+ }+ , let (x, y) = (var "x", var "y")+ (x', y') = (var "x", var "y") in+ TestFormula+ { name = "convert to Chiou 1"+ , formula = exists "x" (x .=. y)+ , expected = [ConvertToChiou (exists "x" (x' .=. y'))]+ }+ , let s = pApp "s"+ s' = pApp "s"+ x' = var "x"+ y' = var "y" in+ TestFormula+ { name = "convert to Chiou 2"+ , formula = s [fApp ("a") [x, y]]+ , expected = [ConvertToChiou (s' [fApp "a" [x', y']])]+ }+ , let s :: [term] -> formula+ s = pApp "s"+ h :: [term] -> formula+ h = pApp "h"+ m :: [term] -> formula+ m = pApp "m"+ s' :: [term] -> formula+ s' = pApp "s"+ h' :: [term] -> formula+ h' = pApp "h"+ m' :: [term] -> formula+ m' = pApp "m"+ x' :: term+ x' = var "x" in+ TestFormula+ { name = "convert to Chiou 3"+ , formula = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x]))+ , expected = [ConvertToChiou (for_all "x" (((s' [x'] .=>. h' [x']) .&. (h' [x'] .=>. m' [x'])) .=>. (s' [x'] .=>. m' [x'])))]+ }+ , let taller :: term -> term -> formula+ taller a b = pApp ("taller" :: p) [a, b]+ wise :: term -> formula+ wise a = pApp ("wise" :: p) [a] in+ TestFormula+ { name = "cnf test 1"+ , formula = for_all "y" (for_all "x" (taller y x .|. wise x) .=>. wise y)+ , expected = [ClauseNormalForm+ (toSS+ [[(pApp ("wise") [var ("y")]),+ ((.~.) (pApp ("taller") [var ("y"),fApp (toSkolem 1) [var ("y")]]))],+ [(pApp ("wise") [var ("y")]),+ ((.~.) (pApp ("wise") [fApp (toSkolem 1) [var ("y")]]))]])]+ }+ , TestFormula+ { name = "cnf test 2"+ , formula = ((.~.) (exists "x" (pApp "s" [x] .&. pApp "q" [x])))+ , expected = [ ClauseNormalForm (toSS + [[((.~.) (pApp ("q") [var ("x")])),+ ((.~.) (pApp ("s") [var ("x")]))]])+ , PrenexNormalForm (for_all "x"+ (((.~.) (pApp ("s") [var ("x")])) .|.+ (((.~.) (pApp ("q") [var ("x")])))))+ {- [[((.~.) (pApp "s" [var "x"])),+ ((.~.) (pApp "q" [var "x"]))]] -}+ ]+ }+ , TestFormula+ { name = "cnf test 3"+ , formula = (for_all "x" (p [x] .=>. (q [x] .|. r [x])))+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [var "x"])),(pApp "q" [var "x"]),(pApp "r" [var "x"])]])]+ }+ , TestFormula+ { name = "cnf test 4"+ , formula = ((.~.) (exists "x" (p [x] .=>. exists "y" (q [y]))))+ , expected = [ClauseNormalForm (toSS [[(pApp "p" [var "x"])],[((.~.) (pApp "q" [var "y"]))]])]+ }+ , TestFormula+ { name = "cnf test 5"+ , formula = (for_all "x" (q [x] .|. r [x] .=>. s [x]))+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "q" [var "x"])),(pApp "s" [var "x"])],[((.~.) (pApp "r" [var "x"])),(pApp "s" [var "x"])]])]+ }+ , TestFormula+ { name = "cnf test 6"+ , formula = (exists "x" (p0 .=>. pApp "f" [x]))+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [])),(pApp "f" [fApp (toSkolem 1) []])]])]+ }+ , let p = pApp "p" []+ f' = pApp "f" [x]+ f = pApp "f" [fApp (toSkolem 1) []] in+ TestFormula+ { name = "cnf test 7"+ , formula = exists "x" (p .<=>. f')+ , expected = [ PrenexNormalForm (exists "x" ((p .&. f') .|. ((((.~.) p) .&. (((.~.) f'))))))+ , SkolemNormalForm ((p .&. f) .|. (((.~.) p) .&. (((.~.) f))))+ , TrivialClauses [(False,S.fromList [((.~.) (pApp ("p") [])),(pApp ("f") [fApp (toSkolem 1) []])]),+ (False,S.fromList [((.~.) (pApp ("f") [fApp (toSkolem 1) []])),(pApp ("p") [])])]+ , ClauseNormalForm (toSS [[(f), ((.~.) p)], [p, ((.~.) f)]])]+ }+ , TestFormula+ { name = "cnf test 8"+ , formula = (for_all "z" (exists "y" (for_all "x" (pApp "f" [x, y] .<=>. (pApp "f" [x, z] .&. ((.~.) (pApp "f" [x, x])))))))+ , expected = [ClauseNormalForm + (toSS [[((.~.) (pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])),(pApp "f" [var "x",var "z"])],+ [((.~.) (pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])),((.~.) (pApp "f" [var "x",var "x"]))],+ [((.~.) (pApp "f" [var "x",var "z"])),(pApp "f" [var "x",var "x"]),(pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])]])]+ }+ , let f = pApp "f" + q = pApp "q"+ sk1 = fApp (toSkolem 1)+ (x, y, z) = (var "x", var "y", var "z") in+ TestFormula+ { name = "cnf test 9"+ , formula = (for_all "x" (for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))))+ , expected = [ClauseNormalForm+ (toSS+ [[(f [z,x]),+ (f [sk1 [x,y],y]),+ ((.~.) (f [z,y]))],+ [(f [z,x]),+ ((.~.) (f [z,y])),+ ((.~.) (f [sk1 [x,y],x])),+ ((.~.) (f [sk1 [x,y],y]))],+ [(f [z,x]),+ ((.~.) (f [z,y])),+ ((.~.) (q [x,y]))],+ [(f [z,y]),+ (f [sk1 [x,y],y]),+ ((.~.) (f [z,x]))],+ [(f [z,y]),+ ((.~.) (f [z,x])),+ ((.~.) (f [sk1 [x,y],x])),+ ((.~.) (f [sk1 [x,y],y]))],+ [(f [z,y]),+ ((.~.) (f [z,x])),+ ((.~.) (q [x,y]))],+ [(f [sk1 [x,y],y]),+ (q [x,y])],+ [(q [x,y]),+ ((.~.) (f [sk1 [x,y],x])),+ ((.~.) (f [sk1 [x,y],y]))]])+ ]+ }+ , TestFormula+ { name = "cnf test 10"+ , formula = (for_all "x" (exists "y" ((p [x, y] .<=. for_all "x" (exists "z" (q [y, x, z]) .=>. r [y])))))+ , expected = [ClauseNormalForm+ (toSS + [[(pApp ("p") [var ("x"),fApp (toSkolem 1) [var ("x")]]),+ (pApp ("q") [fApp (toSkolem 1) [fApp (toSkolem 2) []],fApp (toSkolem 2) [],fApp (toSkolem 3) []])],+ [(pApp ("p") [var ("x"),fApp (toSkolem 1) [var ("x")]]),+ ((.~.) (pApp ("r") [fApp (toSkolem 1) [fApp (toSkolem 2) []]]))]])+ ]+ }+ , TestFormula+ { name = "cnf test 11"+ , formula = (for_all "x" (for_all "z" (p [x, z] .=>. exists "y" ((.~.) (q [x, y] .|. ((.~.) (r [y, z])))))))+ , expected = [ClauseNormalForm+ (toSS + [[((.~.) (pApp "p" [var "x",var "z"])),((.~.) (pApp "q" [var "x",fApp (toSkolem 1) [var "x",var "z"]]))],+ [((.~.) (pApp "p" [var "x",var "z"])),(pApp "r" [fApp (toSkolem 1) [var "x",var "z"],var "z"])]])]+ }+ , TestFormula+ { name = "cnf test 12"+ , formula = ((p0 .=>. q0) .=>. (((.~.) r0) .=>. (s0 .&. t0)))+ , expected = [ClauseNormalForm+ (toSS+ [[(pApp "p" []),(pApp "r" []),(pApp "s" [])],+ [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "s" [])],+ [(pApp "p" []),(pApp "r" []),(pApp "t" [])],+ [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "t" [])]])]+ }+ , let p = pApp "p" []+ true = pApp (fromBool True) []+ false = pApp (fromBool False) [] in+ TestFormula+ { name = "psimplify 50"+ , formula = true .=>. (p .<=>. (p .<=>. false))+ , expected = [ SimplifiedForm (p .<=>. (.~.) p) ] }+ , let true = pApp (fromBool True) []+ false = pApp (fromBool False) [] in+ TestFormula+ { name = "psimplify 51"+ , formula = (((pApp "x" [] .=>. pApp "y" []) .=>. true) .|. false)+ , expected = [ SimplifiedForm (pApp (fromBool True) []) ] }+ , let false = pApp (fromBool False) []+ q = pApp "q" [] in+ TestFormula+ { name = "simplify 140.3"+ , formula = (for_all "x"+ (for_all "y"+ (pApp "p" [var "x"] .|. (pApp "p" [var "y"] .&. false))) .=>.+ (exists "z" q))+ , expected = [ SimplifiedForm ((for_all "x" (pApp "p" [var "x"])) .=>.+ (pApp "q" [])) ] }+ , TestFormula+ { name = "nnf 141.1"+ , formula = ((for_all "x" (pApp "p" [var "x"])) .=>. ((exists "y" (pApp "q" [var "y"])) .<=>. (exists "z" (pApp "p" [var "z"] .&. pApp "q" [var "z"]))))+ , expected = [ NegationNormalForm + ((exists "x" ((.~.) (pApp "p" [var "x"]))) .|.+ ((((exists "y" (pApp "q" [var "y"])) .&. ((exists "z" ((pApp "p" [var "z"]) .&. ((pApp "q" [var "z"])))))) .|.+ (((for_all "y" ((.~.) (pApp "q" [var "y"]))) .&.+ ((for_all "z" (((.~.) (pApp "p" [var "z"])) .|. (((.~.) (pApp "q" [var "z"]))))))))))) ] }+ , TestFormula+ { name = "pnf 144.1"+ , formula = (for_all "x" (pApp "p" [var "x"] .|. pApp "r" [var "y"]) .=>.+ (exists "y" (exists "z" (pApp "q" [var "y"] .|. ((.~.) (exists "z" (pApp "p" [var "z"] .&. pApp "q" [var "z"])))))))+ , expected = [ PrenexNormalForm + (exists "x" + (for_all "z"+ ((((.~.) (pApp "p" [var "x"])) .&. (((.~.) (pApp "r" [var "y"])))) .|.+ (((pApp "q" [var "x"]) .|. ((((.~.) (pApp "p" [var "z"])) .|. (((.~.) (pApp "q" [var "z"])))))))))) ] }+ , let (x, y, u, v) = (var "x", var "y", var "u", var "v")+ fv = fApp (toSkolem 2) [u,x]+ fy = fApp (toSkolem 1) [x] in+ TestFormula+ { name = "snf 150.1"+ , formula = (exists "y" (pApp "<" [x, y] .=>. for_all "u" (exists "v" (pApp "<" [fApp "*" [x, u], fApp "*" [y, v]]))))+ , expected = [ SkolemNormalForm (((.~.) (pApp "<" [x, fy])) .|. pApp "<" [fApp "*" [x, u], fApp "*" [fy, fv]]) ] }+ , let p x = pApp "p" [x]+ q x = pApp "q" [x]+ (x, y, z) = (var "x", var "y", var "z") in+ TestFormula+ { name = "snf 150.2"+ , formula = (for_all "x" (p x .=>. (exists "y" (exists "z" (q y .|. (.~.) (exists "z" (p z .&. (q z))))))))+ , expected = [ SkolemNormalForm (((.~.) (p x)) .|. (q (fApp (toSkolem 1) []) .|. (((.~.) (p z)) .|. ((.~.) (q z))))) ] }+ ]++animalKB :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ (String, [TestFormula formula term v p f])+animalKB =+ let x = var "x"+ y = var "y"+ dog = pApp "Dog"+ cat = pApp "Cat"+ owns = pApp "Owns"+ kills = pApp "Kills"+ animal = pApp "Animal"+ animalLover = pApp "AnimalLover"+ jack = fApp "Jack" []+ tuna = fApp "Tuna" []+ curiosity = fApp "Curiosity" [] in+ ("animal"+ , [ TestFormula+ { formula = exists "x" (dog [x] .&. owns [jack, x]) -- [[Pos 1],[Pos 2]]+ , name = "jack owns a dog"+ , expected = [ClauseNormalForm (toSS [[(pApp "Dog" [fApp (toSkolem 1) []])],[(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])]])]+ -- owns(jack,sK0)+ -- dog (SK0)+ }+ , TestFormula+ { formula = for_all "x" ((exists "y" (dog [y] .&. (owns [x, y]))) .=>. (animalLover [x])) -- [[Neg 1,Neg 2,Pos 3]]+ , name = "dog owners are animal lovers"+ , expected = [ PrenexNormalForm (for_all "x" (for_all "y" ((((.~.) (pApp "Dog" [var "y"])) .|.+ (((.~.) (pApp "Owns" [var "x",var "y"])))) .|.+ ((pApp "AnimalLover" [var "x"])))))+ , ClauseNormalForm (toSS [[((.~.) (pApp "Dog" [var "y"])),((.~.) (pApp "Owns" [var "x",var "y"])),(pApp "AnimalLover" [var "x"])]]) ]+ -- animalLover(X0) | ~owns(X0,sK1(X0)) | ~dog(sK1(X0))+ }+ , TestFormula+ { formula = for_all "x" (animalLover [x] .=>. (for_all "y" ((animal [y]) .=>. ((.~.) (kills [x, y]))))) -- [[Neg 3,Neg 4,Neg 5]]+ , name = "animal lovers don't kill animals"+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "AnimalLover" [var "x"])),((.~.) (pApp "Animal" [var "y"])),((.~.) (pApp "Kills" [var "x",var "y"]))]])]+ -- ~kills(X0,X2) | ~animal(X2) | ~animalLover(sK2(X0))+ }+ , TestFormula+ { formula = (kills [jack, tuna]) .|. (kills [curiosity, tuna]) -- [[Pos 5,Pos 5]]+ , name = "Either jack or curiosity kills tuna"+ , expected = [ClauseNormalForm (toSS [[(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])]])]+ -- kills(curiosity,tuna) | kills(jack,tuna)+ }+ , TestFormula+ { formula = cat [tuna] -- [[Pos 6]]+ , name = "tuna is a cat"+ , expected = [ClauseNormalForm (toSS [[(pApp "Cat" [fApp "Tuna" []])]])]+ -- cat(tuna)+ }+ , TestFormula+ { formula = for_all "x" ((cat [x]) .=>. (animal [x])) -- [[Neg 6,Pos 4]]+ , name = "a cat is an animal"+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "Cat" [var "x"])),(pApp "Animal" [var "x"])]])]+ -- animal(X0) | ~cat(X0)+ }+ ])++animalConjectures :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ [TestFormula formula term v p f]+animalConjectures =+ let kills = pApp "Kills" :: [term] -> formula+ jack = fApp "Jack" [] :: term+ tuna = fApp "Tuna" [] :: term+ curiosity = fApp "Curiosity" [] :: term in++ map (withKB animalKB) $+ [ TestFormula+ { formula = kills [jack, tuna] -- False+ , name = "jack kills tuna"+ , expected =+ [ FirstOrderFormula ((.~.) (((exists "x" ((pApp "Dog" [var ("x")]) .&. ((pApp "Owns" [fApp ("Jack") [],var ("x")])))) .&.+ (((for_all "x" ((exists "y" ((pApp "Dog" [var ("y")]) .&. ((pApp "Owns" [var ("x"),var ("y")])))) .=>.+ ((pApp "AnimalLover" [var ("x")])))) .&.+ (((for_all "x" ((pApp "AnimalLover" [var ("x")]) .=>.+ ((for_all "y" ((pApp "Animal" [var ("y")]) .=>.+ (((.~.) (pApp "Kills" [var ("x"),var ("y")])))))))) .&.+ ((((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]) .|. ((pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.+ (((pApp "Cat" [fApp ("Tuna") []]) .&.+ ((for_all "x" ((pApp "Cat" [var ("x")]) .=>.+ ((pApp "Animal" [var ("x")])))))))))))))) .=>.+ ((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]))))++ , PrenexNormalForm+ (for_all "x"+ (for_all "y"+ (exists "x2"+ ((((pApp ("Dog") [var ("x2")]) .&.+ ((pApp ("Owns") [fApp ("Jack") [],var ("x2")]))) .&.+ ((((((.~.) (pApp ("Dog") [var ("y")])) .|.+ (((.~.) (pApp ("Owns") [var ("x"),var ("y")])))) .|.+ ((pApp ("AnimalLover") [var ("x")]))) .&.+ (((((.~.) (pApp ("AnimalLover") [var ("x")])) .|.+ ((((.~.) (pApp ("Animal") [var ("y")])) .|.+ (((.~.) (pApp ("Kills") [var ("x"),var ("y")])))))) .&.+ ((((pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]) .|.+ ((pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.+ (((pApp ("Cat") [fApp ("Tuna") []]) .&.+ ((((.~.) (pApp ("Cat") [var ("x")])) .|.+ ((pApp ("Animal") [var ("x")]))))))))))))) .&.+ (((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])))))))+ , ClauseNormalForm+ (toSS+ [[(pApp ("Animal") [var ("x")]),+ ((.~.) (pApp ("Cat") [var ("x")]))],+ [(pApp ("AnimalLover") [var ("x")]),+ ((.~.) (pApp ("Dog") [var ("y")])),+ ((.~.) (pApp ("Owns") [var ("x"),var ("y")]))],+ [(pApp ("Cat") [fApp ("Tuna") []])],+ [(pApp ("Dog") [fApp (toSkolem 1) []])],+ [(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),+ (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])],+ [(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])],+ [((.~.) (pApp ("Animal") [var ("y")])),+ ((.~.) (pApp ("AnimalLover") [var ("x")])),+ ((.~.) (pApp ("Kills") [var ("x"),var ("y")]))],+ [((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]))]])+ , ChiouKB1+ (Proof+ Invalid+ (S.fromList + [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])]),+ makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem 1) []])]),+ makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),+ makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]),+ makeINF' ([(pApp ("Animal") [var ("y")]),(pApp ("AnimalLover") [var ("x")]),(pApp ("Kills") [var ("x"),var ("y")])]) ([]),+ makeINF' ([(pApp ("Cat") [var ("x")])]) ([(pApp ("Animal") [var ("x")])]),+ makeINF' ([(pApp ("Dog") [var ("y")]),(pApp ("Owns") [var ("x"),var ("y")])]) ([(pApp ("AnimalLover") [var ("x")])]),+ makeINF' ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]) ([])]))+ ]+ }+ , TestFormula+ { formula = kills [curiosity, tuna] -- True+ , name = "curiosity kills tuna"+ , expected =+ [ ClauseNormalForm+ (toSS+ [[(pApp "Dog" [fApp (toSkolem 1) []])],+ [(pApp "Owns" [fApp ("Jack") [],fApp (toSkolem 1) []])],+ [((.~.) (pApp "Dog" [var ("y")])),+ ((.~.) (pApp "Owns" [var ("x"),var ("y")])),+ (pApp "AnimalLover" [var ("x")])],+ [((.~.) (pApp "AnimalLover" [var ("x")])),+ ((.~.) (pApp "Animal" [var ("y")])),+ ((.~.) (pApp "Kills" [var ("x"),var ("y")]))],+ [(pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]),+ (pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []])],+ [(pApp "Cat" [fApp ("Tuna") []])],+ [((.~.) (pApp "Cat" [var ("x")])),+ (pApp "Animal" [var ("x")])],+ [((.~.) (pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]))]])+ , PropLogicSat True+{-+ , SatSolverCNF [ [Neg 1,Neg 2,Neg 3] -- animallover(x)|animal(y)|kills(x,y)+ , [Neg 4,Pos 5] -- ~cat(x)|animal(x)+ , [Neg 6,Neg 7,Pos 2] -- ~dog(y)|~owns(x,y)|animallover(x)+ , [Neg 8] -- ~kills(curisity,tuna)+ , [Pos 8,Pos 11] -- kills(curiosity,tuna)|kills(jack,tuna)+ , [Pos 9] -- cat(tuna)+ , [Pos 10] -- owns(jack,sk1)+ , [Pos 12] -- dog(sk1)+ ]+-}+ -- I haven't tried to figure out if this is correct, it+ -- probably is because things are working.+ , SatSolverCNF [[Neg 2,Pos 1],[Neg 3,Neg 11,Neg 12],[Neg 4,Neg 5,Pos 3],[Neg 8],[Pos 6],[Pos 7],[Pos 8,Pos 9],[Pos 10]]+ -- It seems like this should be True.+ , SatSolverSat False+ ]+ }+ ]++socratesKB =+ let x = var "x"+ socrates x = pApp "Socrates" [x]+ human x = pApp "Human" [x]+ mortal x = pApp "Mortal" [x] in+ ("socrates"+ , [ TestFormula+ { name = "all humans are mortal"+ , formula = for_all "x" (human x .=>. mortal x)+ , expected = [ClauseNormalForm (toSS [[((.~.) (human x)), mortal x]])] }+ , TestFormula+ { name = "socrates is human"+ , formula = for_all "x" (socrates x .=>. human x)+ , expected = [ClauseNormalForm (toSS [[(.~.) (socrates x), human x]])] }+ ])++{-+socratesConjectures =+ map (withKB socratesKB)+ [ TestFormula+ { formula = for_all' [V "x"] (socrates x .=>. mortal x)+ , name = "socrates is mortal"+ , expected = [ FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))) .&.+ ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Human" [var "x"])))))) .=>.+ ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))))))+ , ClauseNormalForm [[((.~.) (pApp "Human" [var "x2"])),(pApp "Mortal" [var "x2"])],+ [((.~.) (pApp "Socrates" [var "x2"])),(pApp "Human" [var "x2"])],+ [(pApp "Socrates" [fApp (toSkolem 1) [var "x2",var "x2"]])],+ [((.~.) (pApp "Mortal" [fApp (toSkolem 1) [var "x2",var "x2"]]))]]+ , SatPropLogic True ]+ }+ , TestFormula+ { formula = (.~.) (for_all' [V "x"] (socrates x .=>. mortal x))+ , name = "not (socrates is mortal)"+ , expected = [ SatPropLogic False+ , FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))) .&.+ ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Human" [var "x"])))))) .=>.+ (((.~.) (for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Mortal" [var "x"]))))))))+ -- [~human(x) | mortal(x)], [~socrates(Sk1(x,y)) | human(Sk1(x,y))], socrates(Sk1(x,y)), ~mortal(Sk1(x,y))+ -- ~1 | 2, ~3 | 4, 3, ~5?+ , ClauseNormalForm [[((.~.) (pApp "Human" [x])), (pApp "Mortal" [x])],+ [((.~.) (pApp "Socrates" [fApp (toSkolem 1) [x,y]])), (pApp "Human" [fApp (toSkolem 1) [x,y]])],+ [(pApp "Socrates" [fApp (toSkolem 1) [x,y]])], [((.~.) (pApp "Mortal" [fApp (toSkolem 1) [x,y]]))]]+ , ClauseNormalForm [[((.~.) (pApp "Human" [var "x2"])), (pApp "Mortal" [var "x2"])],+ [((.~.) (pApp "Socrates" [var "x2"])), (pApp "Human" [var "x2"])],+ [((.~.) (pApp "Socrates" [var "x"])), (pApp "Mortal" [var "x"])]] ]+ }+ ]+-}++chang43KB = + let e = fApp "e" []+ (x, y, z, u, v, w) = (var "x", var "y", var "z", var "u", var "v", var "w") in+ ("chang example 4.3"+ , [ TestFormula { name = "closure property"+ , formula = for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z]))+ , expected = [] }+ , TestFormula { name = "associativity property"+ , formula = for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [u, z, w] .=>. pApp "P" [x, v, w]) .&.+ for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [x, v, w] .=>. pApp "P" [u, z, w])+ , expected = [] }+ , TestFormula { name = "identity property"+ , formula = (for_all "x" (pApp "P" [x,e,x])) .&. (for_all "x" (pApp "P" [e,x,x]))+ , expected = [] }+ , TestFormula { name = "inverse property"+ , formula = (for_all "x" (pApp "P" [x,fApp "i" [x], e])) .&. (for_all "x" (pApp "P" [fApp "i" [x], x, e]))+ , expected = [] }+ ])++chang43Conjecture :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ TestFormula formula term v p f+chang43Conjecture =+ let e = (fApp "e" [])+ (x, u, v, w) = (var "x", var "u", var "v", var "w") in+ withKB chang43KB $+ TestFormula { name = "G is commutative"+ , formula = for_all "x" (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w]))) + , expected =+ [ FirstOrderFormula + ((.~.) (((for_all' ["x","y"] (exists "z" (pApp "P" [var ("x"),var ("y"),var ("z")]))) .&. ((((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [var ("x"),var ("y"),var ("u")]) .&. ((pApp "P" [var ("y"),var ("z"),var ("v")]))) .&. ((pApp "P" [var ("u"),var ("z"),var ("w")]))) .=>. ((pApp "P" [var ("x"),var ("v"),var ("w")])))) .&. ((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [var ("x"),var ("y"),var ("u")]) .&. ((pApp "P" [var ("y"),var ("z"),var ("v")]))) .&. ((pApp "P" [var ("x"),var ("v"),var ("w")]))) .=>. ((pApp "P" [var ("u"),var ("z"),var ("w")])))))) .&. ((((for_all "x" (pApp "P" [var ("x"),fApp ("e") [],var ("x")])) .&. ((for_all "x" (pApp "P" [fApp ("e") [],var ("x"),var ("x")])))) .&. (((for_all "x" (pApp "P" [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])) .&. ((for_all "x" (pApp "P" [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])))))))))) .=>. ((for_all "x" ((pApp "P" [var ("x"),var ("x"),fApp ("e") []]) .=>. ((for_all' ["u","v","w"] ((pApp "P" [var ("u"),var ("v"),var ("w")]) .=>. ((pApp "P" [var ("v"),var ("u"),var ("w")]))))))))))+ -- (∀x ∀y ∃z P(x,y,z)) &+ -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(u,z,w) | P(x,v,w)) &+ -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(x,v,w) | P(u,z,w)) &+ -- (∀x P(x,e,x)) &+ -- (∀x P(e,x,x)) &+ -- (∀x P(x,i[x],e)) &+ -- (∀x P(i[x],x,e)) &+ -- (∃x P(x,x,e) & (∃u∃v∃w P(u,v,w) & ~P(v,u,w)))+ , NegationNormalForm+ (((for_all "x"+ (for_all "y"+ (exists "z"+ (pApp ("P") [var ("x"),var ("y"),var ("z")])))) .&.+ ((((for_all "x"+ (for_all "y"+ (for_all "z"+ (for_all "u"+ (for_all "v"+ (for_all "w"+ (((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+ ((pApp ("P") [var ("x"),var ("v"),var ("w")]))))))))) .&.+ ((for_all "x"+ (for_all "y"+ (for_all "z"+ (for_all "u"+ (for_all "v"+ (for_all "w"+ (((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+ ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))))))))) .&.+ ((((for_all "x" (pApp ("P") [var ("x"),fApp ("e") [],var ("x")])) .&.+ ((for_all "x" (pApp ("P") [fApp ("e") [],var ("x"),var ("x")])))) .&.+ (((for_all "x" (pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])) .&.+ ((for_all "x" (pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])))))))))) .&.+ ((exists "x"+ ((pApp ("P") [var ("x"),var ("x"),fApp ("e") []]) .&.+ ((exists "u"+ (exists "v"+ (exists "w"+ ((pApp ("P") [var ("u"),var ("v"),var ("w")]) .&.+ (((.~.) (pApp ("P") [var ("v"),var ("u"),var ("w")]))))))))))))+ , PrenexNormalForm+ (for_all "x"+ (for_all "y"+ (for_all "z"+ (for_all "u"+ (for_all "v"+ (for_all "w"+ (exists "z2"+ (exists "x2"+ (exists "u2"+ (exists "v2"+ (exists "w2"+ (((pApp ("P") [var ("x"),var ("y"),var ("z2")]) .&.+ ((((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+ ((pApp ("P") [var ("x"),var ("v"),var ("w")]))) .&.+ ((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+ ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))) .&.+ ((((pApp ("P") [var ("x"),fApp ("e") [],var ("x")]) .&.+ ((pApp ("P") [fApp ("e") [],var ("x"),var ("x")]))) .&.+ (((pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []]) .&.+ ((pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []]))))))))) .&.+ (((pApp ("P") [var ("x2"),var ("x2"),fApp ("e") []]) .&.+ (((pApp ("P") [var ("u2"),var ("v2"),var ("w2")]) .&.+ (((.~.) (pApp ("P") [var ("v2"),var ("u2"),var ("w2")])))))))))))))))))))+ , SkolemNormalForm+ (((pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]]) .&.+ ((((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+ ((pApp ("P") [var ("x"),var ("v"),var ("w")]))) .&.+ ((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+ (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+ (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+ ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))) .&.+ ((((pApp ("P") [var ("x"),fApp ("e") [],var ("x")]) .&.+ ((pApp ("P") [fApp ("e") [],var ("x"),var ("x")]))) .&.+ (((pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []]) .&.+ ((pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []]))))))))) .&.+ (((pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []]) .&.+ (((pApp ("P") [fApp (toSkolem 3) [],fApp (toSkolem 4) [],fApp (toSkolem 5) []]) .&.+ (((.~.) (pApp ("P") [fApp (toSkolem 4) [],fApp (toSkolem 3) [],fApp (toSkolem 5) []]))))))))+ , SkolemNumbers (S.fromList [1,2,3,4,5])+ -- From our algorithm++ , ClauseNormalForm+ (toSS + [[(pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]])],+ [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+ ((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])),+ ((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])),+ (pApp ("P") [var ("x"),var ("v"),var ("w")])],+ [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+ ((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])),+ ((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])),+ (pApp ("P") [var ("u"),var ("z"),var ("w")])],+ [(pApp ("P") [var ("x"),fApp ("e") [],var ("x")])],+ [(pApp ("P") [fApp ("e") [],var ("x"),var ("x")])],+ [(pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])],+ [(pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])],+ [(pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []])],+ [(pApp ("P") [fApp (toSkolem 3) [],fApp (toSkolem 4) [],fApp (toSkolem 5) []])],+ [((.~.) (pApp ("P") [fApp (toSkolem 4) [],fApp (toSkolem 3) [],fApp (toSkolem 5) []]))]])++ -- From the book+{-+ , let (a, b, c) = + (fApp (toSkolem 3) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")],+ fApp (toSkolem 4) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")],+ fApp (toSkolem 5) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")]) in+ ClauseNormalForm+ [[(pApp "P" [var "x",var "y",fApp (toSkolem 1) [var "x",var "y"]])],+ [((.~.) (pApp "P" [var "x",var "y",var "u"])),+ ((.~.) (pApp "P" [var "y",var "z",var "v"])),+ ((.~.) (pApp "P" [var "u",var "z",var "w"])),+ (pApp "P" [var "x",var "v",var "w"])],+ [((.~.) (pApp "P" [var "x",var "y",var "u"])),+ ((.~.) (pApp "P" [var "y",var "z",var "v"])),+ ((.~.) (pApp "P" [var "x",var "v",var "w"])),+ (pApp "P" [var "u",var "z",var "w"])],+ [(pApp "P" [var "x",fApp "e" [],var "x"])],+ [(pApp "P" [fApp "e" [],var "x",var "x"])],+ [(pApp "P" [var "x",fApp "i" [var "x"],fApp "e" []])],+ [(pApp "P" [fApp "i" [var "x"],var "x",fApp "e" []])],+ [(pApp "P" [var "x",+ var "x",+ fApp "e" []])],+ [(pApp "P" [a, b, c])],+ [((.~.) (pApp "P" [b, a, c]))]]+-}+ ]+ }++{-+% ghci+> :load Test/Data.hs+> :m +Logic.FirstOrder+> :m +Logic.Normal+> let f = (.~.) (conj (map formula (snd chang43KB)) .=>. formula chang43Conjecture)+> putStrLn (runNormal (cnfTrace f))+-}++chang43ConjectureRenamed :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ TestFormula formula term v p f+chang43ConjectureRenamed =+ let e = fApp "e" []+ (x, y, z, u, v, w) = (var "x", var "y", var "z", var "u", var "v", var "w")+ (u2, v2, w2, x2, y2, z2, u3, v3, w3, x3, y3, z3, x4, x5, x6, x7, x8) =+ (var "u2", var "v2", var "w2", var "x2", var "y2", var "z2", var "u3", var "v3", var "w3", var "x3", var "y3", var "z3", var "x4", var "x5", var "x6", var "x7", var "x8") in+ TestFormula { name = "chang 43 renamed"+ , formula = (.~.) ((for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z])) .&.+ for_all' ["x2", "y2", "z2", "u", "v", "w"] (pApp "P" [x2, y2, u] .&. pApp "P" [y2, z2, v] .&. pApp "P" [u, z2, w] .=>. pApp "P" [x2, v, w]) .&.+ for_all' ["x3", "y3", "z3", "u2", "v2", "w2"] (pApp "P" [x3, y3, u2] .&. pApp "P" [y3, z3, v2] .&. pApp "P" [x3, v2, w2] .=>. pApp "P" [u2, z3, w2]) .&.+ for_all "x4" (pApp "P" [x4,e,x4]) .&.+ for_all "x5" (pApp "P" [e,x5,x5]) .&.+ for_all "x6" (pApp "P" [x6,fApp "i" [x6], e]) .&.+ for_all "x7" (pApp "P" [fApp "i" [x7], x7, e])) .=>.+ (for_all "x8" (pApp "P" [x8, x8, e] .=>. (for_all' ["u3", "v3", "w3"] (pApp "P" [u3, v3, w3] .=>. pApp "P" [v3, u3, w3])))))+ , expected =+ [ FirstOrderFormula+ ((.~.) ((((((((for_all' ["x","y"] (exists "z" (pApp "P" [var "x",var "y",var "z"]))) .&.+ ((for_all' ["x2","y2","z2","u","v","w"] ((((pApp "P" [var "x2",var "y2",var "u"]) .&.+ ((pApp "P" [var "y2",var "z2",var "v"]))) .&.+ ((pApp "P" [var "u",var "z2",var "w"]))) .=>.+ ((pApp "P" [var "x2",var "v",var "w"])))))) .&.+ ((for_all' ["x3","y3","z3","u2","v2","w2"] ((((pApp "P" [var "x3",var "y3",var "u2"]) .&.+ ((pApp "P" [var "y3",var "z3",var "v2"]))) .&.+ ((pApp "P" [var "x3",var "v2",var "w2"]))) .=>.+ ((pApp "P" [var "u2",var "z3",var "w2"])))))) .&.+ ((for_all "x4" (pApp "P" [var "x4",fApp "e" [],var "x4"])))) .&.+ ((for_all "x5" (pApp "P" [fApp "e" [],var "x5",var "x5"])))) .&.+ ((for_all "x6" (pApp "P" [var "x6",fApp "i" [var "x6"],fApp "e" []])))) .&.+ ((for_all "x7" (pApp "P" [fApp "i" [var "x7"],var "x7",fApp "e" []])))) .=>.+ ((for_all "x8" ((pApp "P" [var "x8",var "x8",fApp "e" []]) .=>.+ ((for_all' ["u3","v3","w3"] ((pApp "P" [var "u3",var "v3",var "w3"]) .=>.+ ((pApp "P" [var "v3",var "u3",var "w3"]))))))))))+ , let a = fApp (toSkolem 3) []+ b = fApp (toSkolem 4) []+ c = fApp (toSkolem 5) [] in+ ClauseNormalForm+ (toSS+ [[(pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]])],+ [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+ ((.~.) (pApp ("P") [var ("y"),var ("z2"),var ("v")])),+ ((.~.) (pApp ("P") [var ("u"),var ("z2"),var ("w")])),+ (pApp ("P") [var ("x"),var ("v"),var ("w")])],+ [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+ ((.~.) (pApp ("P") [var ("y"),var ("z2"),var ("v")])),+ ((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])),+ (pApp ("P") [var ("u"),var ("z2"),var ("w")])],+ [(pApp ("P") [var ("x"),fApp ("e") [],var ("x")])],+ [(pApp ("P") [fApp ("e") [],var ("x"),var ("x")])],+ [(pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])],+ [(pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])],+ [(pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []])],+ [(pApp ("P") [a,b,c])],+ [((.~.) (pApp ("P") [b,a,c]))]]) + ]+ }++withKB :: forall formula term v p f. (FirstOrderFormula formula term v p f) =>+ (String, [TestFormula formula term v p f]) -> TestFormula formula term v p f -> TestFormula formula term v p f+withKB (kbName, knowledge) conjecture =+ conjecture { name = name conjecture ++ " with " ++ kbName ++ " knowledge base"+ -- Here we say that the conjunction of the knowledge+ -- base formula implies the conjecture. We prove the+ -- theorem by showing that the negation is+ -- unsatisfiable.+ , formula = (.~.) (conj (map formula knowledge) .=>. formula conjecture)}+ where+ conj [] = error "conj []"+ conj [x] = x+ conj (x:xs) = x .&. conj xs++kbKnowledge :: forall formula term v p f. (FirstOrderFormula formula term v p f) =>+ (String, [TestFormula formula term v p f]) -> (String, [formula])+kbKnowledge kb = (fst (kb :: (String, [TestFormula formula term v p f])), map formula (snd kb))++proofs :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+ [TestProof formula term v]+proofs =+ let -- dog = pApp "Dog" :: [term] -> formula+ -- cat = pApp "Cat" :: [term] -> formula+ -- owns = pApp "Owns" :: [term] -> formula+ kills = pApp "Kills" :: [term] -> formula+ -- animal = pApp "Animal" :: [term] -> formula+ -- animalLover = pApp "AnimalLover" :: [term] -> formula+ socrates = pApp "Socrates" :: [term] -> formula+ -- human = pApp "Human" :: [term] -> formula+ mortal = pApp "Mortal" :: [term] -> formula++ jack :: term+ jack = fApp "Jack" []+ tuna :: term+ tuna = fApp "Tuna" []+ curiosity :: term+ curiosity = fApp "Curiosity" [] in++ [ TestProof+ { proofName = "prove jack kills tuna"+ , proofKnowledge = kbKnowledge (animalKB :: (String, [TestFormula formula term v p f]))+ , conjecture = kills [jack, tuna]+ , proofExpected = + [ ChiouKB (S.fromList+ [WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Dog" [fApp (toSkolem 1) []])]), wiIdent = 1},+ WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])]), wiIdent = 1},+ WithId {wiItem = INF (S.fromList [(pApp "Dog" [var "y"]),(pApp "Owns" [var "x",var "y"])]) (S.fromList [(pApp "AnimalLover" [var "x"])]), wiIdent = 2},+ WithId {wiItem = INF (S.fromList [(pApp "Animal" [var "y"]),(pApp "AnimalLover" [var "x"]),(pApp "Kills" [var "x",var "y"])]) (S.fromList []), wiIdent = 3},+ WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])]), wiIdent = 4},+ WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Cat" [fApp "Tuna" []])]), wiIdent = 5},+ WithId {wiItem = INF (S.fromList [(pApp "Cat" [var "x"])]) (S.fromList [(pApp "Animal" [var "x"])]), wiIdent = 6}])+ , ChiouResult (False,+ (S.fromList+ [(inf' [(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])] [],fromList []),+ (inf' [] [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])],fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+ (inf' [(pApp "AnimalLover" [fApp "Curiosity" []]),(pApp "Cat" [fApp "Tuna" []])] [],fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList []),+ (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+ (inf' [(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),+ (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList []),+ (inf' [(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+ (inf' [(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList [])]))+ ]+ }+ , TestProof+ { proofName = "prove curiosity kills tuna"+ , proofKnowledge = kbKnowledge (animalKB :: (String, [TestFormula formula term v p f]))+ , conjecture = kills [curiosity, tuna]+ , proofExpected =+ [ ChiouKB (S.fromList+ [WithId {wiItem = inf' [] [(pApp "Dog" [fApp (toSkolem 1) []])], wiIdent = 1},+ WithId {wiItem = inf' [] [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])], wiIdent = 1},+ WithId {wiItem = inf' [(pApp "Dog" [var "y"]),+ (pApp "Owns" [var "x",var "y"])] [(pApp "AnimalLover" [var "x"])], wiIdent = 2},+ WithId {wiItem = inf' [(pApp "Animal" [var "y"]),+ (pApp "AnimalLover" [var "x"]),+ (pApp "Kills" [var "x",var "y"])] [], wiIdent = 3},+ WithId {wiItem = inf' [] [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),+ (pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])], wiIdent = 4},+ WithId {wiItem = inf' [] [(pApp "Cat" [fApp "Tuna" []])], wiIdent = 5},+ WithId {wiItem = inf' [(pApp "Cat" [var "x"])] [(pApp "Animal" [var "x"])], wiIdent = 6}])+ , ChiouResult (True,+ S.fromList + [(makeINF' ([]) ([]),fromList []),+ (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem 1) []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem 1) []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]) ([]),fromList []),+ (makeINF' ([(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])+ ]+ }+{-+ -- Seems not to terminate+ , let (x, u, v, w, e) = (var "x", var "u", var "v", var "w", var "e") in+ TestProof+ { proofName = "chang example 4.3"+ , proofKnowledge = (fst chang43KB, map (convertFOF id id id . formula) (snd chang43KB))+ , conjecture = for_all' ["x"] (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w])))+ , proofExpected =+ [ChiouResult (True, [])]+ }+-}+ , let x = var "x" in+ TestProof+ { proofName = "socrates is mortal"+ , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+ , conjecture = for_all "x" (socrates [x] .=>. mortal [x])+ , proofExpected = + [ ChiouKB (S.fromList+ [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+ WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+ , ChiouResult (True,+ S.fromList + [(makeINF' ([]) ([]),fromList []),+ (makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([(pApp ("Mortal") [fApp (toSkolem 3) []])]) ([]),fromList [])])]+ }+ , let x = var "x" in+ TestProof+ { proofName = "socrates is not mortal"+ , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+ , conjecture = (.~.) (for_all "x" (socrates [x] .=>. mortal [x]))+ , proofExpected = + [ ChiouKB (S.fromList+ [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+ WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+ , ChiouResult (False+ ,(S.fromList [(inf' [(pApp "Socrates" [var "x"])] [(pApp "Mortal" [var "x"])],fromList [("x",var "x")])]))]+ }+ , let x = var "x" in+ TestProof+ { proofName = "socrates exists and is not mortal"+ , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+ , conjecture = (.~.) (exists "x" (socrates [x]) .&. for_all "x" (socrates [x] .=>. mortal [x]))+ , proofExpected = + [ ChiouKB (S.fromList+ [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+ WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+ , ChiouResult (False,+ S.fromList [(makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem 3) []])]),fromList []),+ (makeINF' ([(pApp ("Socrates") [var ("x")])]) ([(pApp ("Mortal") [var ("x")])]),fromList [("x",var ("x"))])])+ ]+ }+ ]++inf' = makeINF'++toLL = map S.toList . S.toList+toSS = S.fromList . map S.fromList
+ Test/Logic.hs view
@@ -0,0 +1,436 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,+ ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall -Wwarn -fno-warn-name-shadowing -fno-warn-orphans #-}+module Test.Logic (tests) where++import Data.Logic.Classes.Arity (Arity(arity))+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), showFirstOrder, freeVars, substitute)+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.Classes.Variable (Variable)+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (runNormal)+import Data.Logic.Satisfiable (theorem, inconsistant)+import Data.Logic.Test (V(..), AtomicFunction(..), Pr, TFormula, TTerm)+import qualified Data.Set as Set+import Data.String (IsString(fromString))+import PropLogic (PropForm(..), TruthTable, truthTable)+import qualified TextDisplay as TD+import Test.HUnit++-- |Don't use this at home! It breaks type safety, fromString "True"+-- fromBool True.+instance Boolean String where+ fromBool = show++tests :: Test+tests = TestLabel "Logic" $ TestList (precTests ++ theoremTests)++formCase :: FirstOrderFormula TFormula TTerm V Pr AtomicFunction =>+ String -> TFormula -> TFormula -> Test+formCase s expected input = TestLabel s $ TestCase (assertEqual s expected input)++precTests :: [Test]+precTests =+ [ formCase "Logic - prec test 1"+ (a .&. (b .|. c))+ (a .&. b .|. c)+ -- You can't apply .~. without parens:+ -- :type (.~. a) -> (FormulaPF -> t) -> t+ -- :type ((.~.) a) -> FormulaPF+ , formCase "Logic - prec test 2"+ (((.~.) a) .&. b)+ ((.~.) a .&. b)+ -- I switched the precedence of .&. and .|. from infixl to infixr to get+ -- some of the test cases to match the answers given on the miami.edu site,+ -- but maybe I should switch them back and adjust the answer given in the+ -- test case.+ , formCase "Logic - prec test 3"+ ((a .&. b) .&. c) -- infixl, with infixr we get (a .&. (b .&. c))+ (a .&. b .&. c)+ , TestCase (assertEqual "Logic - Find a free variable"+ (freeVars (for_all "x" (x .=. y) :: TFormula))+ (Set.singleton "y"))+ , TestCase (assertEqual "Logic - Substitute a variable"+ (map sub+ [ for_all "x" (x .=. y) {- :: Formula String String -}+ , for_all "y" (x .=. y) {- :: Formula String String -} ])+ [ for_all "x" (x .=. z) :: TFormula+ , for_all "y" (z .=. y) :: TFormula ])+ ]+ where+ sub f = substitute (head . Set.toList . freeVars $ f) (var "z") f+ a = pApp ("a") []+ b = pApp ("b") []+ c = pApp ("c") []++x :: TTerm+x = var (fromString "x")+y :: TTerm+y = var (fromString "y")+z :: TTerm+z = var (fromString "z")++-- |Here is an example of automatic conversion from a FirstOrderFormula+-- instance to a PropositionalFormula instance. The result is PropForm+-- a where a is the original type, but the a values will always be+-- "atomic" formulas, never the operators which can be converted into+-- the corresponding operator of a PropositionalFormula instance.+{-+test9a :: Test+test9a = TestCase + (assertEqual "Logic - convert to PropLogic"+ expected+ (flatten (cnf' (for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))))))+ where+ f = pApp "f"+ q = pApp "q"+ expected :: PropForm TFormula+ expected = CJ [DJ [N (A (pApp ("q") [var (V "x"),var (V "y")])),+ N (A (pApp ("f") [var (V "z"),var (V "x")])),+ A (pApp ("f") [var (V "z"),var (V "y")])],+ DJ [N (A (pApp ("q") [var (V "x"),var (V "y")])),+ N (A (pApp ("f") [var (V "z"),var (V "y")])),+ A (pApp ("f") [var (V "z"),var (V "x")])],+ DJ [A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")]),+ A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")]),+ A (pApp ("q") [var (V "x"),var (V "y")])],+ DJ [N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")])),+ A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")]),+ A (pApp ("q") [var (V "x"),var (V "y")])],+ DJ [A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")]),+ N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")])),+ A (pApp ("q") [var (V "x"),var (V "y")])],+ DJ [N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")])),+ N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")])),+ A (pApp ("q") [var (V "x"),var (V "y")])]]++moveQuantifiersOut1 :: Test+moveQuantifiersOut1 =+ formCase "Logic - moveQuantifiersOut1"+ (for_all "x2" ((pApp ("p") [var ("x2")]) .&. ((pApp ("q") [var ("x")]))))+ (prenexNormalForm (for_all "x" (pApp (fromString "p") [x]) .&. (pApp (fromString "q") [x])))++skolemize1 :: Test+skolemize1 =+ formCase "Logic - skolemize1" expected formula+ where+ expected :: TFormula+ expected = for_all [V "y",V "z"] (for_all [V "v"] (pApp "P" [fApp (toSkolem 1) [], y, z, fApp ((toSkolem 2)) [y, z], v, fApp (toSkolem 3) [y, z, v]]))+ formula :: TFormula+ formula = (snf' (exists ["x"] (for_all ["y", "z"] (exists ["u"] (for_all ["v"] (exists ["w"] (pApp "P" [x, y, z, u, v, w])))))))++skolemize2 :: Test+skolemize2 =+ formCase "Logic - skolemize2" expected formula+ where+ expected :: TFormula+ expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [],y])+ formula :: TFormula+ formula = snf' (exists ["x"] (for_all ["y"] (pApp "loves" [x, y])))++skolemize3 :: Test+skolemize3 =+ formCase "Logic - skolemize3" expected formula+ where+ expected :: TFormula+ expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [y],y])+ formula :: TFormula+ formula = snf' (for_all ["y"] (exists ["x"] (pApp "loves" [x, y])))+-}+{-+inf1 :: Test+inf1 =+ formCase "Logic - inf1" expected formula+ where+ expected :: TFormula+ expected = ((pApp ("p") [var ("x")]) .=>. (((pApp ("q") [var ("x")]) .|. ((pApp ("r") [var ("x")])))))+ formula :: {- ImplicativeNormalFormula inf (C.Sentence V String AtomicFunction) (C.Term V AtomicFunction) V String AtomicFunction => -} TFormula+ formula = convertFOF id id id (implicativeNormalForm (convertFOF id id id (for_all ["x"] (p [x] .=>. (q [x] .|. r [x]))) :: C.Sentence V String AtomicFunction) :: C.Sentence V String AtomicFunction)+-}++instance Arity String where+ arity _ = Nothing++theoremTests :: [Test]+theoremTests =+ let s = pApp "S"+ h = pApp "H"+ m = pApp "M" in+ [ let formula = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>.+ (s [x] .=>. m [x])) in+ TestCase (assertEqual "Logic - theorem test 1"+ (True,([],Just (CJ []),[([],True)]))+{-+ (True,+ ([(pApp ("H") [var (V "x")]),(pApp ("M") [var (V "x")]),(pApp ("S") [var (V "x")])],+ Just (CJ [DJ [A (pApp ("S") [var (V "x")]),+ A (pApp ("H") [var (V "x")]),+ N (A (pApp ("S") [var (V "x")])),+ A (pApp ("M") [var (V "x")])],+ DJ [N (A (pApp ("H") [var (V "x")])),+ A (pApp ("H") [var (V "x")]),+ N (A (pApp ("S") [var (V "x")])),+ A (pApp ("M") [var (V "x")])],+ DJ [A (pApp ("S") [var (V "x")]),+ N (A (pApp ("M") [var (V "x")])),+ N (A (pApp ("S") [var (V "x")])),+ A (pApp ("M") [var (V "x")])],+ DJ [N (A (pApp ("H") [var (V "x")])),+ N (A (pApp ("M") [var (V "x")])),+ N (A (pApp ("S") [var (V "x")])),+ A (pApp ("M") [var (V "x")])]]),+ [([False,False,False],True),+ ([False,False,True],True),+ ([False,True,False],True),+ ([False,True,True],True),+ ([True,False,False],True),+ ([True,False,True],True),+ ([True,True,False],True),+ ([True,True,True],True)]))+-}+ (runNormal (theorem formula), table formula))+ , TestCase (assertEqual "Logic - theorem test 1a"+ (False,+ False,+ ([(pApp1 ("H") (fApp (toSkolem 1) [])),+ (pApp1 ("M") (var ("y"))),+ (pApp1 ("M") (fApp (toSkolem 1) [])),+ (pApp1 ("S") (var ("y"))),+ (pApp1 ("S") (fApp (toSkolem 1) []))],+ Just (CJ [DJ [A (pApp1 ("H") (fApp (toSkolem 1) [])),+ A (pApp1 ("M") (var ("y"))),+ A (pApp1 ("S") (fApp (toSkolem 1) [])),+ N (A (pApp1 ("S") (var ("y"))))],+ DJ [A (pApp1 ("M") (var ("y"))),+ A (pApp1 ("S") (fApp (toSkolem 1) [])),+ N (A (pApp1 ("M") (fApp (toSkolem 1) []))),+ N (A (pApp1 ("S") (var ("y"))))],+ DJ [A (pApp1 ("M") (var ("y"))),+ N (A (pApp1 ("H") (fApp (toSkolem 1) []))),+ N (A (pApp1 ("M") (fApp (toSkolem 1) []))),+ N (A (pApp1 ("S") (var ("y"))))]]),+ [([False,False,False,False,False],True),+ ([False,False,False,False,True],True),+ ([False,False,False,True,False],False),+ ([False,False,False,True,True],True),+ ([False,False,True,False,False],True),+ ([False,False,True,False,True],True),+ ([False,False,True,True,False],False),+ ([False,False,True,True,True],True),+ ([False,True,False,False,False],True),+ ([False,True,False,False,True],True),+ ([False,True,False,True,False],True),+ ([False,True,False,True,True],True),+ ([False,True,True,False,False],True),+ ([False,True,True,False,True],True),+ ([False,True,True,True,False],True),+ ([False,True,True,True,True],True),+ ([True,False,False,False,False],True),+ ([True,False,False,False,True],True),+ ([True,False,False,True,False],True),+ ([True,False,False,True,True],True),+ ([True,False,True,False,False],True),+ ([True,False,True,False,True],True),+ ([True,False,True,True,False],False),+ ([True,False,True,True,True],False),+ ([True,True,False,False,False],True),+ ([True,True,False,False,True],True),+ ([True,True,False,True,False],True),+ ([True,True,False,True,True],True),+ ([True,True,True,False,False],True),+ ([True,True,True,False,True],True),+ ([True,True,True,True,False],True),+ ([True,True,True,True,True],True)]))+ + (let formula = (for_all "x" ((s [x] .=>. h [x]) .&. (h [x] .=>. m [x]))) .=>.+ (for_all "y" (s [y] .=>. m [y])) in+ (runNormal (theorem formula), runNormal (inconsistant formula), table formula)))+ + , TestCase (assertEqual "Logic - socrates is mortal, truth table"+ ([(pApp1 ("H") (var ("x"))),+ (pApp1 ("M") (var ("x"))),+ (pApp1 ("S") (var ("x")))],+ Just (CJ [DJ [A (pApp1 ("H") (var ("x"))),N (A (pApp1 ("S") (var ("x"))))],+ DJ [A (pApp1 ("M") (var ("x"))),N (A (pApp1 ("H") (var ("x"))))],+ DJ [A (pApp1 ("M") (var ("x"))),N (A (pApp1 ("S") (var ("x"))))]]),+ [([False,False,False],True),+ ([False,False,True],False),+ ([False,True,False],True),+ ([False,True,True],False),+ ([True,False,False],False),+ ([True,False,True],False),+ ([True,True,False],True),+ ([True,True,True],True)])+ -- This formula has separate variables for each of the+ -- three beliefs. To combine these into an argument+ -- we would wrap a single exists around them all and+ -- remove the existing ones, substituting that one+ -- variable into each formula.+ (table (for_all "x" (s [x] .=>. h [x]) .&.+ for_all "y" (h [y] .=>. m [y]) .&.+ for_all "z" (s [z] .=>. m [z]))))++ , TestCase (assertEqual "Logic - socrates is not mortal"+ (False,+ False,+ ([(pApp ("H") [var ("x")]),+ (pApp ("M") [var ("x")]),+ (pApp ("S") [var ("x")]),+ (pApp ("S") [fApp ("socrates") []])],+ Just (CJ [DJ [A (pApp ("H") [var ("x")]),N (A (pApp ("S") [var ("x")]))],+ DJ [A (pApp ("M") [var ("x")]),N (A (pApp ("H") [var ("x")]))],+ DJ [A (pApp ("S") [fApp ("socrates") []])],+ DJ [N (A (pApp ("M") [var ("x")])),N (A (pApp ("S") [var ("x")]))]]),+ [([False,False,False,False],False),+ ([False,False,False,True],True),+ ([False,False,True,False],False),+ ([False,False,True,True],False),+ ([False,True,False,False],False),+ ([False,True,False,True],True),+ ([False,True,True,False],False),+ ([False,True,True,True],False),+ ([True,False,False,False],False),+ ([True,False,False,True],False),+ ([True,False,True,False],False),+ ([True,False,True,True],False),+ ([True,True,False,False],False),+ ([True,True,False,True],True),+ ([True,True,True,False],False),+ ([True,True,True,True],False)]),+ toSS [[(pApp ("H") [var ("x")]),((.~.) (pApp ("S") [var ("x")]))],+ [(pApp ("M") [var ("x")]),((.~.) (pApp ("H") [var ("x")]))],+ [(pApp ("S") [fApp ("socrates") []])],+ [((.~.) (pApp ("M") [var ("x")])),((.~.) (pApp ("S") [var ("x")]))]])+ -- This represents a list of beliefs like those in our+ -- database: socrates is a man, all men are mortal,+ -- each with its own quantified variable. In+ -- addition, we have an inconsistant belief, socrates+ -- is not mortal. If we had a single variable this+ -- would be inconsistant, but as it stands it is an+ -- invalid argument, there are both 0 and 1 lines in+ -- the truth table. If we go through the table and+ -- eliminate the lines where S(SkZ(x,y)) is true but M(SkZ(x,y)) is+ -- false (for any x) and those where H(x) is true but+ -- M(x) is false, the remaining lines would all be zero,+ -- the argument would be inconsistant (an anti-theorem.)+ -- How can we modify the formula to make these lines 0?+ (let (formula :: TFormula) =+ for_all "x" ((s [x] .=>. h [x]) .&.+ (h [x] .=>. m [x]) .&.+ (m [x] .=>. ((.~.) (s [x])))) .&.+ (s [fApp "socrates" []]) in+ (runNormal (theorem formula), runNormal (inconsistant formula), table formula, runNormal (clauseNormalForm formula) :: Set.Set (Set.Set TFormula))))+ , let (formula :: TFormula) =+ (for_all "x" (pApp "L" [var "x"] .=>. pApp "F" [var "x"]) .&. -- All logicians are funny+ exists "x" (pApp "L" [var "x"])) .=>. -- Someone is a logician+ (.~.) (exists "x" (pApp "F" [var "x"])) -- Someone / Nobody is funny+ input = table formula+ expected = ([(pApp ("F") [var ("x2")]),+ (pApp ("F") [fApp (toSkolem 1) []]),+ (pApp ("L") [var ("x")]),+ (pApp ("L") [fApp (toSkolem 1) []])],+ Just (CJ [DJ [A (pApp1 ("L") (fApp (toSkolem 1) [])),N (A (pApp1 ("F") (var ("x2")))),N (A (pApp1 ("L") (var ("x"))))],+ DJ [N (A (pApp1 ("F") (var ("x2")))),N (A (pApp1 ("F") (fApp (toSkolem 1) []))),N (A (pApp1 ("L") (var ("x"))))]]),+ [([False,False,False,False],True),+ ([False,False,False,True],True),+ ([False,False,True,False],True),+ ([False,False,True,True],True),+ ([False,True,False,False],True),+ ([False,True,False,True],True),+ ([False,True,True,False],True),+ ([False,True,True,True],True),+ ([True,False,False,False],True),+ ([True,False,False,True],True),+ ([True,False,True,False],False),+ ([True,False,True,True],True),+ ([True,True,False,False],True),+ ([True,True,False,True],True),+ ([True,True,True,False],False),+ ([True,True,True,True],False)])+ in TestCase (assertEqual "Logic - gensler189" expected input)+ , let (formula :: TFormula) =+ (for_all "x" (pApp "L" [var "x"] .=>. pApp "F" [var "x"]) .&. -- All logicians are funny+ exists "y" (pApp "L" [var (fromString "y")])) .=>. -- Someone is a logician+ (.~.) (exists "z" (pApp "F" [var "z"])) -- Someone / Nobody is funny+ input = table formula+ expected :: TruthTable TFormula+ expected = ([(pApp1 ("F") (var ("z"))),(pApp1 ("F") (fApp (toSkolem 1) [])),(pApp1 ("L") (var ("y"))),(pApp1 ("L") (fApp (toSkolem 1) []))],Just (CJ [DJ [A (pApp1 ("L") (fApp (toSkolem 1) [])),N (A (pApp1 ("F") (var ("z")))),N (A (pApp1 ("L") (var ("y"))))],DJ [N (A (pApp1 ("F") (var ("z")))),N (A (pApp1 ("F") (fApp (toSkolem 1) []))),N (A (pApp1 ("L") (var ("y"))))]]),[([False,False,False,False],True),([False,False,False,True],True),([False,False,True,False],True),([False,False,True,True],True),([False,True,False,False],True),([False,True,False,True],True),([False,True,True,False],True),([False,True,True,True],True),([True,False,False,False],True),([True,False,False,True],True),([True,False,True,False],False),([True,False,True,True],True),([True,True,False,False],True),([True,True,False,True],True),([True,True,True,False],False),([True,True,True,True],False)])+ in TestCase (assertEqual "Logic - gensler189 renamed" expected input)+ ]++toSS :: Ord a => [[a]] -> Set.Set (Set.Set a)+toSS = Set.fromList . map Set.fromList++{-+theorem5 =+ TestCase (assertEqual "Logic - theorm test 2"+ (Just True)+ (theorem ((.~.) ((for_all "x" (((s [x] .=>. h [x]) .&.+ (h [x] .=>. m [x]))) .&.+ exists "x" (s [x] .&.+ ((.~.) (m [x]))))))))+-}++instance TD.Display TFormula where+ textFrame x = [showFirstOrder x]+{-+ textFrame x = [quickShow x]+ where+ quickShow =+ foldF (\ _ -> error "Expecting atoms")+ (\ _ _ _ -> error "Expecting atoms")+ (\ _ _ _ -> error "Expecting atoms")+ (\ t1 op t2 -> quickShowTerm t1 ++ quickShowOp op ++ quickShowTerm t2)+ (\ p ts -> quickShowPred p ++ "(" ++ intercalate "," (map quickShowTerm ts) ++ ")")+ quickShowTerm =+ foldT quickShowVar+ (\ f ts -> quickShowFn f ++ "(" ++ intercalate "," (map quickShowTerm ts) ++ ")")+ quickShowVar v = show v+ quickShowPred s = s+ quickShowFn (AtomicFunction s) = s+ quickShowOp (:=:) = "="+ quickShowOp (:!=:) = "!="+-}++{-+-- Truth table tests, find a more reasonable result value than [String].++(theorem1a, theorem1b, theorem1c, theorem1d) =+ ( TestCase (assertEqual "Logic - truth table 1"+ (Just ["foo"])+ (prepare (for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x]))) >>=+ return . TD.textFrame . truthTable)) )+ where s = pApp "S"+ h = pApp "H"+ m = pApp "M"++type FormulaPF = Formula String String+type F = PropForm FormulaPF++prepare :: FormulaPF -> F+prepare formula = ({- flatten . -} fromJust . toPropositional convertA . cnf . (.~.) $ formula)++convertA = Just . A+-}++table :: forall formula term v p f. (FirstOrderFormula formula term v p f, Literal formula term v p f,+ Ord formula, Skolem f, IsString v, Variable v, TD.Display formula) =>+ formula -> TruthTable formula+table f =+ -- truthTable :: Ord a => PropForm a -> TruthTable a+ tt cnf'+ where+ tt :: PropForm formula -> TruthTable formula+ tt = truthTable+ cnf' :: PropForm formula+ cnf' = CJ (map (DJ . map n) cnf)+ cnf :: [[formula]]+ cnf = fromSS (runNormal (clauseNormalForm f))+ fromSS = map Set.toList . Set.toList+ n f = (if negated f then N . A . (.~.) else A) $ f
+ Test/TPTP.hs view
@@ -0,0 +1,22 @@+module Test.TPTP where+ +import Codec.TPTP (Formula)+import Data.Logic.FirstOrder (conj)+import Data.Logic.Instances.TPTP+import Data.Logic.Monad (runNormal)+import Data.Logic.Logic (Logic ((.~.), (.=>.)))+import Data.Logic.Normal (cnfTrace)+import Data.Logic.Test (TestFormula(formula))+import Test.Data (chang43KB, chang43Conjecture)+import Test.HUnit++tests :: Test+tests = TestLabel "TPTP" $ TestList [tptp]++tptp :: Test+tptp =+ TestCase (assertEqual "tptp cnf trace" "abc" (runNormal (cnfTrace f)))+ where+ f :: Formula+ f = (.~.) (conj (map formula (snd (chang43KB :: (String, [TestFormula Formula])))) .=>.+ formula chang43Conjecture)
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name: logic-classes-Version: 0.47+Version: 0.48 License: BSD3 Author: David Fox <dsf@seereason.com> Maintainer: SeeReason Partners <partners@seereason.com>@@ -49,3 +49,4 @@ Executable tests Main-Is: Test/Test.hs Build-Depends: HUnit+ Other-Modules: Test.Chiou0 Test.Data Test.Logic, Test.TPTP