diff --git a/Data/Logic/Instances/TPTP.hs b/Data/Logic/Instances/TPTP.hs deleted file mode 100644 --- a/Data/Logic/Instances/TPTP.hs +++ /dev/null @@ -1,183 +0,0 @@ -{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, - RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeSynonymInstances, UndecidableInstances #-} -{-# OPTIONS -fno-warn-missing-signatures -fno-warn-orphans #-} -module Logic.Instances.TPTP where - -import Codec.TPTP (F(..), Formula, BinOp(..), V(..), T(..), Term0(..), AtomicWord(..), Formula0(..), InfixPred(..)) -import qualified Codec.TPTP as TPTP -import Control.Monad.Identity (Identity(..)) -import Data.Char (isDigit, ord) -import Data.Generics (Data, Typeable) -import Data.String (IsString(..)) -import qualified Logic.FirstOrder as Logic -import Logic.FirstOrder (FirstOrderFormula(..), Term(..), Pretty(..), Predicate(..), Variable(next), pApp) -import qualified Logic.Logic as Logic -import Logic.Logic (Negatable(..), Logic(..), Boolean(..)) -import qualified Logic.Propositional as Logic -import Text.PrettyPrint (text) - --- |Generate a series of variable names. -instance Variable V where - one = V "VS1" - next (V s) = - V (case break (not . isDigit) (reverse s) of - ("", "SV") -> "VS1" - (digits, "SV") -> "VS" ++ show (1 + read (reverse digits) :: Int) - _ -> "VS1") - -instance Logic.Arity AtomicWord where - arity _ = Nothing - -instance Logic.Pretty V where - pretty (V s) = text s - -mn = 'x' -pref = 'x' -mx = 'z' -cnt = ord mx - ord mn + 1 - --- |TPTP's Term type has two extra constructors that can be represented --- using this augmented atomic function application type. -data AtomicFunction - = Atom AtomicWord - | StringLit String - | NumberLit Double - | Skolem V - deriving (Eq, Ord, Show, Data, Typeable) - -instance IsString AtomicFunction where - fromString = Atom . AtomicWord - -instance Logic.Skolem AtomicFunction where - toSkolem = Skolem . V . ("sK" ++) . show - fromSkolem (Skolem (V s)) = Just (read (drop 2 s) :: Int) - fromSkolem _ = Nothing - --- |This is not a safe way to implement booleans. -instance Logic.Boolean AtomicWord where - fromBool = AtomicWord . show - -instance Logic.Pretty AtomicFunction where - pretty (Atom w) = Logic.pretty w - pretty (StringLit s) = text (show s) - pretty (NumberLit n) = text (show n) - pretty (Skolem (V s)) = text ("sK" ++ s) - -instance Logic.Pretty AtomicWord where - pretty (AtomicWord s) = text s - -instance Logic.Negatable Formula where - negated (F (Identity ((:~:) x))) = not (negated x) - negated _ = False - (.~.) (F (Identity ((:~:) x))) = x - (.~.) x = (.~.) x - --- |If this looks confusing, it is because TPTP has the same operators --- as Logic, the .&. on the left is the Logic method name and .&. on --- the right is the TPTP function. -instance Logic.Logic Formula where - x .<=>. y = x .<=>. y - x .=>. y = x .=>. y - x .<=. y = x .<=. y - x .|. y = x .|. y - x .&. y = x .&. y - x .<~>. y = x .<~>. y - x .~|. y = x .~|. y - x .~&. y = x .~&. y - --- |For types designed to represent first order (predicate) logic, it --- is easiest to make the atomic type the same as the formula type, --- and then raise an error if we see unexpected non-atomic formulas. -instance Logic.PropositionalFormula Formula Formula where - atomic (F (Identity (InfixPred t1 (:=:) t2))) = t1 .=. t2 - atomic (F (Identity (InfixPred t1 (:!=:) t2))) = t1 .!=. t2 - atomic (F (Identity (PredApp p ts))) = pApp p ts - atomic _ = error "atomic method of PropositionalFormula for TPTP: invalid argument" - -- Use the TPTP fold to implement the Logic fold. This means - -- building wrappers around some of the functions so that when - -- the wrappers are passed TPTP types they turn them into Logic - -- values to pass to the argument functions. - foldF0 c a form = - TPTP.foldF n' q' b' i' p' (unwrapF' form) - where q' = error "TPTP Formula with quantifier passed to foldF0" - n' f = c ((Logic.:~:) f) - b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2) - b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1) - b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2) - b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2) - -- The :~&: operator is not present in the Logic BinOp type, - -- so we need to use the equivalent ~(a&b) - b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2)) - b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2) - b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2)) - b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2))) - i' t1 (:=:) t2 = a (F (Identity (InfixPred t1 (:=:) t2))) - i' t1 (:!=:) t2 = a (F (Identity (InfixPred t1 (:!=:) t2))) - p' p ts = a (F (Identity (PredApp p ts))) - unwrapF' (F x) = F x -- copoint x - -instance Logic.FirstOrderFormula Formula (T Identity) V AtomicWord AtomicFunction where - for_all vars x = for_all vars x - exists vars x = exists vars x - -- Use the TPTP fold to implement the Logic fold. This means - -- building wrappers around some of the functions so that when - -- the wrappers are passed TPTP types they turn them into Logic - -- values to pass to the argument functions. - foldF q c p form = - TPTP.foldF n' q' b' i' p' (unwrapF' form) - where q' op (v:vs) form' = - let op' = case op of - TPTP.All -> Logic.All - TPTP.Exists -> Logic.Exists in - q op' v (foldr (\ v' f -> Logic.quant op' v' f) form' vs) - q' _ [] form' = foldF q c p form' - n' f = c ((Logic.:~:) f) - b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2) - b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1) - b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2) - b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2) - -- The :~&: operator is not present in the Logic BinOp type, - -- so we need to somehow use the equivalent ~(a&b) - b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2)) - b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2) - b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2)) - b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2))) - i' t1 (:=:) t2 = p (Equal t1 t2) - i' t1 (:!=:) t2 = p (NotEqual t1 t2) -- TPTP.foldF n' q' b' i' p' ((.~.) (t1 .=. t2)) - p' pr ts = p (Apply pr ts) - unwrapF' (F x) = F x -- copoint x - zipF = error "Unimplemented: Logic.Instances.TPTP.zipF" - x .=. y = x .=. y - x .!=. y = x .!=. y - pApp0 p = TPTP.pApp p [] - pApp1 p a = TPTP.pApp p [a] - pApp2 p a b = TPTP.pApp p [a,b] - pApp3 p a b c = TPTP.pApp p [a,b,c] - pApp4 p a b c d = TPTP.pApp p [a,b,c,d] - pApp5 p a b c d e = TPTP.pApp p [a,b,c,d,e] - pApp6 p a b c d e f = TPTP.pApp p [a,b,c,d,e,f] - pApp7 p a b c d e f g = TPTP.pApp p [a,b,c,d,e,f,g] - -instance (Eq AtomicFunction, Logic.Skolem AtomicFunction) => Logic.Term (T Identity) V AtomicFunction where - foldT v fa term = - -- We call the foldT function from the TPTP package here, which - -- has a different signature from the foldT method we are - -- implementing. The two extra term types in TPTP are represented - -- here as additional values in the AtomicFunction type. - TPTP.foldT string double v atom (unwrapT' term) - where atom w ts = fa (Atom w) ts - string s = fa (StringLit s) [] - double n = fa (NumberLit n) [] - unwrapT' (T x) = T x -- copoint x - zipT = error "Unimplemented: Logic.Instances.TPTP.zipT" - var = var - fApp x args = - case x of - Atom w -> TPTP.fApp w args - StringLit s -> T {runT = Identity (DistinctObjectTerm s)} - NumberLit n -> T {runT = Identity (NumberLitTerm n)} - Skolem (V s) -> TPTP.fApp (AtomicWord ("Sk(" ++ s ++ ")")) args - ---deriving instance Show TPTP.Term ---deriving instance (Show t, Show f) => Show (TPTP.Formula0 t f) ---deriving instance Show t => Show (TPTP.Term0 t) diff --git a/Data/Logic/Types/FirstOrderPublic.hs b/Data/Logic/Types/FirstOrderPublic.hs --- a/Data/Logic/Types/FirstOrderPublic.hs +++ b/Data/Logic/Types/FirstOrderPublic.hs @@ -8,8 +8,6 @@ module Data.Logic.Types.FirstOrderPublic ( Formula(..) - , N.PTerm(..) - , Bijection(..) ) where import Data.Data (Data) @@ -32,6 +30,7 @@ import Data.Typeable (Typeable) import Happstack.Data (deriveNewData) +-- |Convert between the public and internal representations. class Bijection p i where public :: i -> p intern :: p -> i @@ -96,9 +95,13 @@ c' combine1 combine2 = c (public combine1) (public combine2) -- |Here are the magic Ord and Eq instances -instance (FirstOrderFormula (Formula v p f) (N.PTerm v f) v p f, +instance ({- FirstOrderFormula (Formula v p f) (N.PTerm v f) v p f, Literal (N.Formula v p f) (N.PTerm v f) v p f, - FirstOrderFormula (N.Formula v p f) (N.PTerm v f) v p f, + FirstOrderFormula (N.Formula v p f) (N.PTerm v f) v p f, -} + Data v, Data f, Data p, + Ord v, Ord p, Ord f, + Show v, Show p, Show f, + Arity p, Boolean p, Skolem f, Variable v, Ord (N.Formula v p f)) => Ord (Formula v p f) where compare a b = let (a' :: Set (ImplicativeForm (N.Formula v p f))) = runNormal (implicativeNormalForm (intern a :: N.Formula v p f)) diff --git a/Test/Chiou0.hs b/Test/Chiou0.hs deleted file mode 100644 --- a/Test/Chiou0.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-# 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' (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' (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' (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"]))] diff --git a/Test/Data.hs b/Test/Data.hs deleted file mode 100644 --- a/Test/Data.hs +++ /dev/null @@ -1,1077 +0,0 @@ -{-# 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 diff --git a/Test/Logic.hs b/Test/Logic.hs deleted file mode 100644 --- a/Test/Logic.hs +++ /dev/null @@ -1,436 +0,0 @@ -{-# 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 diff --git a/Test/TPTP.hs b/Test/TPTP.hs deleted file mode 100644 --- a/Test/TPTP.hs +++ /dev/null @@ -1,22 +0,0 @@ -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) diff --git a/debian/changelog b/debian/changelog deleted file mode 100644 --- a/debian/changelog +++ /dev/null @@ -1,368 +0,0 @@ -haskell-logic-classes (0.44) unstable; urgency=low - - * Major re-organization of modules. - - -- David Fox Sun, 09 Oct 2011 17:31:36 -0700 - -haskell-logic (0.43) unstable; urgency=low - - * Move Propositional modules into Data.Logic.Propositional. - * Add a Native instance for PropositionalFormula. - * Add a Normal in the Propositional directory - * Add clauseNormalForm and disjunctiveNormalForm for Propositional - * Add clauseNormalFormAlt which is an alternate implementation of - clauseNormalForm, I'm not sure if it gives results that are actually - different or just look different, but it makes cabal-debian work. - - -- David Fox Thu, 29 Sep 2011 05:56:41 -0700 - -haskell-logic (0.42) unstable; urgency=low - - * Derive the show instance for ImplicativeNormalForm rather than - making a custom one. - - -- David Fox Fri, 23 Sep 2011 16:43:09 -0700 - -haskell-logic (0.41) unstable; urgency=low - - * Add field accessors to Proof type. - * Finish show implementation for Proof - - -- David Fox Mon, 08 Aug 2011 08:32:56 -0700 - -haskell-logic (0.40) unstable; urgency=low - - * Remove NoProof constructor from Proof type - we only need this in - the augumented Proof' type in the ontology package. - * Add prettyProof and prettyINF to Data.Logic.Pretty. - - -- David Fox Sat, 06 Aug 2011 06:28:20 -0700 - -haskell-logic (0.39) unstable; urgency=low - - * Move Proof type from ontology to logic. - - -- David Fox Thu, 04 Aug 2011 07:13:00 -0700 - -haskell-logic (0.38) unstable; urgency=low - - * Remove the triple of function parameters for converting formulas to - literals, these were all invariably id. - - -- David Fox Tue, 02 Aug 2011 07:34:54 -0700 - -haskell-logic (0.37) unstable; urgency=low - - * Add an Ord instance to ProofResult so we can insert proofs into sets. - - -- David Fox Mon, 01 Aug 2011 09:51:59 -0700 - -haskell-logic (0.36) unstable; urgency=low - - * Move module Test.Types to Data.Logic.Test and export so that clients - of this package can use the definitions to create test cases. - - -- David Fox Sun, 24 Jul 2011 10:45:50 -0700 - -haskell-logic (0.35) unstable; urgency=low - - * Remove the Pretty class. Pretty printing of a type is application - specific, so the type class doesn't make sense. Instead add function - parameters to prettyForm et. al. to convert the primitive types to - Doc. - - -- David Fox Fri, 22 Jul 2011 09:01:45 -0700 - -haskell-logic (0.34) unstable; urgency=low - - * Allow .=. literals in the Native instance. This required a fix to the - resolution prover so that it never did substitutions based on an - equality predicate which had the same lhs and rhs. - - -- David Fox Thu, 21 Jul 2011 22:30:14 -0700 - -haskell-logic (0.33) unstable; urgency=low - - * Move the modules into the Data heirarchy. - - -- David Fox Sun, 17 Jul 2011 07:29:49 -0700 - -haskell-logic (0.32) unstable; urgency=low - - * Add a Pred class to describe predicate application - * Split pretty printing and show into a module. - - -- David Fox Sat, 16 Jul 2011 15:24:43 -0700 - -haskell-logic (0.31) unstable; urgency=low - - * Create a second instance of FirstOrderFormula in the module - Logic.Instances.Public, with Eq and Ord instances that use - the normal form to detect formulas that are equivalent under - identity transforms. - * Export the Bijection class which converts between the public - and internal formula types. - - -- David Fox Wed, 06 Jul 2011 12:46:45 -0700 - -haskell-logic (0.30) unstable; urgency=low - - * Simplify the parameters of the ImplicativeNormalForm type in the - native instance, move it to Logic.Normal and eliminate the - ImplicativeNormalFormula class. - * Don't require all formula and term types to be instances of Ord, - we can just specify it in the functions that need it. - - -- David Fox Sat, 02 Jul 2011 09:20:57 -0700 - -haskell-logic (0.29) unstable; urgency=low - - * Ported to safe-copy - - -- Jeremy Shaw Fri, 17 Jun 2011 11:18:32 -0500 - -haskell-logic (0.28) unstable; urgency=low - - * Switch the order of some constructors so that defaultValue of - Formula gives us a simpler value. - - -- David Fox Sun, 01 May 2011 11:36:12 -0700 - -haskell-logic (0.27) unstable; urgency=low - - * Moved JSON instances back to seereason. - - -- David Fox Wed, 13 Apr 2011 20:53:42 -0700 - -haskell-logic (0.26) unstable; urgency=low - - * Add JSON instances. - - -- David Fox Mon, 04 Apr 2011 07:21:25 -0600 - -haskell-logic (0.25) unstable; urgency=low - - * Disable the (unused) Logic-TPTP instance, it is blocking the - ghc7 build. - - -- David Fox Sat, 30 Oct 2010 10:35:35 -0700 - -haskell-logic (0.24) unstable; urgency=low - - * Add a missing paren in the pretty printing and show instances. - - -- David Fox Wed, 20 Oct 2010 21:17:34 -0700 - -haskell-logic (0.23) unstable; urgency=low - - * Add a "one" method to the Variable class which returns any instance of - the class, preferably some general purpose variable name like "x". - - -- David Fox Wed, 06 Oct 2010 12:28:38 -0700 - -haskell-logic (0.22) unstable; urgency=low - - * Instead of making variables instances of Enum and having non-working - fromEnum and toEnum methods, create a class Var with only a "next" - method. - * Add an Arity class and make it a super class of the predicate types. - * Replace the pApp method with pApp0, pApp1, pApp2 ... pApp7, add a - pApp function that checks the predicate arity and dispatches to the - correct method, or throws an error. - * Add withUnivQuant to look at the list of universally quantified - variables wrapped around a formula. - - -- David Fox Fri, 03 Sep 2010 12:36:25 -0700 - -haskell-logic (0.21.2) unstable; urgency=low - - * Fix a bug in fromFirstOrder - * Add Logic.Set.cartesianProduct, use to implement allpairs - * Add purednf and implement purecnf in terms of purednf. - - -- David Fox Mon, 30 Aug 2010 15:44:10 -0700 - -haskell-logic (0.21) unstable; urgency=low - - * Rename the *Logic classes -> *Formula - * Split a NormalFormula class out of FirstOrderFormula, use it as - the result of the clauseNormalForm and implicativeNormalForm - functions. - - -- David Fox Sun, 29 Aug 2010 14:27:34 -0700 - -haskell-logic (0.20) unstable; urgency=low - - * Reduce the number of arguments to foldF to three, one for quantifiers, - one for combining formulas, one for predicates. - * Add a Predicate type for a temporary representation of a predicate and - its arguments, this is the type now passed to foldF. - - -- David Fox Mon, 23 Aug 2010 22:14:22 -0700 - -haskell-logic (0.19) unstable; urgency=low - - * Extensive work on polymorphic version of Resolution prover and test cases. - * Emergency check-in due to dying disk. - * Implement skolemization and cnf algorithms from Harrison book. - - -- David Fox Tue, 17 Aug 2010 14:55:39 -0700 - -haskell-logic (0.18) unstable; urgency=low - - * Remove the Predicate and Proposition synonyms for Formula, they - seem likely to confuse. - - -- David Fox Wed, 28 Jul 2010 09:30:41 -0700 - -haskell-logic (0.17) unstable; urgency=low - - * Make all the normal form code polymorphic. - - -- David Fox Mon, 26 Jul 2010 08:05:24 -0700 - -haskell-logic (0.16) unstable; urgency=low - - * Move important super classes from the individual functions to the type - class FirstOrderLogic: Eq p, Boolean p, Eq f, Skolem f. - * Implement a default method for .!=. - * Remove two "quick simplifications" from Logic.NormalForm.distributeDisjuncts - because they assume Eq formula, which isn't really well defined. Can these - make any difference anyway once we reach CNF? - * Rename convertPred -> convertFOF to match class name change. - - -- David Fox Sat, 10 Jul 2010 22:25:18 -0700 - -haskell-logic (0.15) unstable; urgency=low - - * Rename PredicateLogic -> FirstOrderLogic - * Add a Logic.Prover module with a function to load a knowledgebase. - - -- David Fox Thu, 08 Jul 2010 16:00:35 -0700 - -haskell-logic (0.14) unstable; urgency=low - - * Fix skolem handling. Use a Skolem class to convert between Ints - and skolem functions, and a HasSkolem class to obtain numbers for - skolem functions from a monad. - * Integrate Chiou Prover package into this one. We need to mix - pieces of the two. - - -- David Fox Thu, 08 Jul 2010 12:47:23 -0700 - -haskell-logic (0.13) unstable; urgency=low - - * Implement polymorphic version of implicativeNormalForm. - - -- David Fox Tue, 06 Jul 2010 22:39:55 -0700 - -haskell-logic (0.12) unstable; urgency=low - - * Parameterize the variable type v in the PredicateLogic class and - the Formula type in the Parameterized instance. - * Reduce the number of functional dependencies in the PredicateLogic - class, this allows us to create two instances that use the same - types for any of v, p, or f. - - -- David Fox Tue, 06 Jul 2010 17:52:37 -0700 - -haskell-logic (0.11) unstable; urgency=low - - * Modify the Skolem class so it uses a monad to generate new names - for skolem functions. This corresponds to the technique used - by what is now our only working example of a first order logic - theorem prover, the new Chiou package. - - -- David Fox Mon, 05 Jul 2010 12:46:08 -0700 - -haskell-logic (0.10) unstable; urgency=low - - * Add an instance for the Charles Chiou first order logic prover. - - -- David Fox Mon, 05 Jul 2010 09:03:04 -0700 - -haskell-logic (0.9) unstable; urgency=low - - * Add a Logic.Satisfiable module, containing functions theorem, - inconsistant, and invalid. - - -- David Fox Fri, 02 Jul 2010 11:34:38 -0700 - -haskell-logic (0.8) unstable; urgency=low - - * Modify skolemize so it leaves the universal quantifiers on its - result, and add a function removeUniversal to remove them. We - envision having a use for those quantifiers some time soon. - * Use standard names for the various normal forms, move Logic.CNF - to Logic.NormalForm. - - -- David Fox Wed, 30 Jun 2010 18:28:00 -0700 - -haskell-logic (0.7) unstable; urgency=low - - * Change the order of substitution function arguments from (new, old) - to (old, new), to match the notation generally used in textbooks. - - -- David Fox Wed, 30 Jun 2010 08:58:54 -0700 - -haskell-logic (0.6.1) unstable; urgency=low - - * Fix a bug in substituteTerm and re-implement skolemize. - - -- David Fox Wed, 30 Jun 2010 06:43:50 -0700 - -haskell-logic (0.6) unstable; urgency=low - - * Split a Logic class out of PropositionalLogic and make it the ancestor - of PropositionalLogic and PredicateLogic. This way we can eliminate - the horrible atom parameter from the PredicateLogic type. - * Add a Skolem v f class to encapsulate conversion of variables to - skolem functions. - - -- David Fox Mon, 28 Jun 2010 06:34:43 -0700 - -haskell-logic (0.5.1) unstable; urgency=low - - * Rename variables in the moveQuantifiersOut operation of cnf to - avoid collisions later. - * Add an Enum instance for the V type so we can find fresh variables, - and new functions for finding the quantified variables and all the - variables in a formula. - - -- David Fox Sun, 27 Jun 2010 07:00:49 -0700 - -haskell-logic (0.5) unstable; urgency=low - - * Export distributeDisjuncts - - -- David Fox Fri, 25 Jun 2010 14:13:44 -0700 - -haskell-logic (0.4) unstable; urgency=low - - * Add documentation - * Remove the normalize function - * Remove the AtomicWord type (use the equivalent in Logic-TPTP.) - * Make some derived methods into functions. - - -- David Fox Fri, 25 Jun 2010 09:32:22 -0700 - -haskell-logic (0.3) unstable; urgency=low - - * Eliminate the use of the unicode characters for for_all and - exists, they make the amd64 version of haddock crash. - - -- David Fox Thu, 24 Jun 2010 13:46:42 -0700 - -haskell-logic (0.2) unstable; urgency=low - - * Add an Ord instance to AtomicFormula to satisfy the requirements - of the satisfiable function in PropLogic. - - -- David Fox Thu, 24 Jun 2010 10:08:42 -0700 - -haskell-logic (0.1) unstable; urgency=low - - * Debianization generated by cabal-debian - - -- David Fox Wed, 23 Jun 2010 14:19:18 -0700 - diff --git a/debian/compat b/debian/compat deleted file mode 100644 --- a/debian/compat +++ /dev/null @@ -1,1 +0,0 @@ -7 diff --git a/debian/control b/debian/control deleted file mode 100644 --- a/debian/control +++ /dev/null @@ -1,83 +0,0 @@ -Source: haskell-logic-classes -Priority: optional -Section: misc -Maintainer: David Fox -Build-Depends: debhelper (>= 7.0), - haskell-devscripts (>= 0.6.15+nmu7), - hscolour, - cdbs, - ghc (>= 6.8), - ghc-prof, - libghc-hunit-prof, - libghc-fgl-prof, - libghc-happstack-data-prof, - libghc-incremental-sat-solver-prof, - libghc-proplogic-prof, - libghc-mtl-prof, - libghc-safecopy-prof, - libghc-set-extra-prof, - libghc-syb-with-class-prof, - libghc-text-prof -Build-Depends-Indep: ghc-doc, - haddock, - libghc-hunit-doc, - libghc-fgl-doc, - libghc-happstack-data-doc, - libghc-incremental-sat-solver-doc, - haskell-proplogic-doc, - libghc-mtl-doc, - libghc-safecopy-doc, - libghc-set-extra-doc, - libghc-syb-with-class-doc, - libghc-text-doc -Standards-Version: 3.8.1 - -Package: libghc-logic-classes-dev -Architecture: any -Section: haskell -Depends: ${haskell:Depends}, - ${misc:Depends} -Conflicts: libghc-logic-dev -Provides: libghc-logic-dev -Replaces: libghc-logic-dev -Description: Library for unifying various treatments of propositional and first order logic - Library for unifying various treatments of propositional and first order logic - . - Author: David Fox - Upstream-Maintainer: SeeReason Partners - . - This package contains the normal library files. - -Package: libghc-logic-classes-prof -Architecture: any -Section: haskell -Depends: ${haskell:Depends}, - ${misc:Depends}, - libghc-logic-dev -Conflicts: libghc-logic-prof -Provides: libghc-logic-prof -Replaces: libghc-logic-prof -Description: Library for unifying various treatments of propositional and first order logic - Library for unifying various treatments of propositional and first order logic - . - Author: David Fox - Upstream-Maintainer: SeeReason Partners - . - This package contains the libraries compiled with profiling enabled. - -Package: libghc-logic-classes-doc -Architecture: all -Section: doc -Depends: ${haskell:Depends}, - ${misc:Depends}, - ghc-doc -Conflicts: libghc-logic-doc -Provides: libghc-logic-doc -Replaces: libghc-logic-doc -Description: Library for unifying various treatments of propositional and first order logic - Library for unifying various treatments of first order logic - . - Author: David Fox - Upstream-Maintainer: SeeReason Partners - . - This package contains the documentation files. diff --git a/debian/copyright b/debian/copyright deleted file mode 100644 --- a/debian/copyright +++ /dev/null @@ -1,1 +0,0 @@ -BSD diff --git a/debian/rules b/debian/rules deleted file mode 100644 --- a/debian/rules +++ /dev/null @@ -1,7 +0,0 @@ -#!/usr/bin/make -f -include /usr/share/cdbs/1/rules/debhelper.mk -include /usr/share/cdbs/1/class/hlibrary.mk - -# How to install an extra file into the documentation package -#binary-fixup/libghc6-Logic-doc:: -# echo "Some informative text" > debian/libghc6-Logic-doc/usr/share/doc/libghc6-Logic-doc/AnExtraDocFile diff --git a/logic-classes.cabal b/logic-classes.cabal --- a/logic-classes.cabal +++ b/logic-classes.cabal @@ -1,9 +1,9 @@ Name: logic-classes -Version: 0.44 +Version: 0.45 License: BSD3 Author: David Fox Maintainer: SeeReason Partners -Synopsis: Symbolic logic support - a class framework, example instances, polymorphic implementations +Synopsis: Support for propositional and first order logic, normal forms, and a resolution theorem prover. Description: Package to support Propositional and First Order Logic. It includes classes representing the different types of formulas and terms, some instances of those classes for types used in other logic libraries, and implementations of