{-# 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