packages feed

logic-classes 1.5 → 1.5.1

raw patch · 23 files changed

+398/−3492 lines, 23 filesdep +logic-classesdep −fgldep −syb-with-classdep −textdep ~PropLogic

Dependencies added: logic-classes

Dependencies removed: fgl, syb-with-class, text

Dependency ranges changed: PropLogic

Files

Data/Boolean/SatSolver.hs view
@@ -110,7 +110,7 @@ -- and only if that fails. --  isSolvable :: SatSolver -> Bool-isSolvable = not . null . solve+isSolvable = not . (null :: [a] -> Bool) . solve   -- private helper functions
+ Data/Logic/HUnit.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE MultiParamTypeClasses, RankNTypes #-}+module Data.Logic.HUnit+    ( Test(..)+    , Assertion+    , T.assertEqual+    , convert+    , TestFormula+    , TestFormulaEq+    ) where++import Data.Logic.Classes.Apply (Apply)+import Data.Logic.Classes.Equals (AtomEq)+import Data.Logic.Classes.FirstOrder (FirstOrderFormula)+import Data.Logic.Classes.Term (Term)+import Data.Logic.Types.Harrison.FOL (Function(..))+import Data.String (IsString(fromString))+import qualified Test.HUnit as T++type Assertion t = IO ()++-- | HUnit Test type with an added phantom type parameter.  To run+-- such a test you use the convert function below:+-- @+--   :load Data.Logic.Tests.Harrison.Meson+--   :m +Data.Logic.Tests.HUnit+--   :m +Test.HUnit+--   runTestTT (convert tests)+-- @+data Test t+  = TestCase (Assertion t)+  | TestList [Test t]+  | TestLabel String (Test t)+  | Test0 T.Test++convert :: Test t -> T.Test+convert (TestCase assertion) = T.TestCase assertion+convert (TestList tests) = T.TestList (map convert tests)+convert (TestLabel label test) = T.TestLabel label (convert test)+convert (Test0 test) = test++class (FirstOrderFormula formula atom v,+       Apply atom p term,+       Term term v f,+       Eq formula, Ord formula, Show formula,+       Eq p,+       IsString v, IsString p, IsString f, Ord f, Ord p,+       Eq term, Show term, Ord term,+       Show v) => TestFormula formula atom term v p f++class (FirstOrderFormula formula atom v,+       AtomEq atom p term,+       Term term v f,+       Eq formula, Ord formula, Show formula,+       Eq p,+       IsString v, IsString p, IsString f, Ord f, Ord p,+       Eq term, Show term, Ord term,+       Show v) => TestFormulaEq formula atom term v p f++{-+type Test' = forall formula atom term v p f. TestFormula formula atom term v p f => Test formula+type Formula' = forall formula atom term v p f. TestFormula formula atom term v p f => formula+type TestEq' = forall formula atom term v p f. TestFormulaEq formula atom term v p f => Test formula+type FormulaEq' = forall formula atom term v p f. TestFormulaEq formula atom term v p f => formula+-}++instance IsString Function where+    fromString = FName
Data/Logic/Harrison/DP.hs view
@@ -12,7 +12,7 @@ import Data.Logic.Harrison.Lib (allpairs, maximize', minimize', defined, setmapfilter, (|->)) import Data.Logic.Harrison.Prop (negative, positive, trivial, tautology, cnf) import Data.Logic.Harrison.PropExamples (Atom(..), N, prime)-import Data.Logic.Tests.HUnit+import Data.Logic.HUnit import Data.Logic.Types.Propositional (Formula(..)) import qualified Data.Map as Map import qualified Data.Set.Extra as Set
+ Data/Logic/Instances/Chiou.hs view
@@ -0,0 +1,306 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,+             RankNTypes, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall -Wwarn -fno-warn-orphans -fno-warn-missing-signatures #-}+module Data.Logic.Instances.Chiou+    ( Sentence(..)+    , CTerm(..)+    , Connective(..)+    , Quantifier(..)+    , ConjunctiveNormalForm(..)+    , NormalSentence(..)+    , NormalTerm(..)+    , toSentence+    , fromSentence+    ) where++import Data.Generics (Data, Typeable)+import Data.Logic.Classes.Apply (Apply(..), Predicate, pApp)+import Data.Logic.Classes.Atom (Atom)+import Data.Logic.Classes.Combine (Combinable(..), BinOp(..), Combination(..))+import Data.Logic.Classes.Constants (Constants(..), asBool, true, false)+import Data.Logic.Classes.Equals (AtomEq(..), (.=.))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), Quant(..), quant', prettyFirstOrder, fixityFirstOrder, foldAtomsFirstOrder, mapAtomsFirstOrder)+import Data.Logic.Classes.Formula (Formula(..))+import Data.Logic.Classes.Negate (Negatable(..), (.~.))+import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..))+import Data.Logic.Classes.Term (Term(..), Function)+import Data.Logic.Classes.Variable (Variable)+import Data.Logic.Classes.Propositional (PropositionalFormula(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.String (IsString(..))++data Sentence v p f+    = Connective (Sentence v p f) Connective (Sentence v p f)+    | Quantifier Quantifier [v] (Sentence v p f)+    | Not (Sentence v p f)+    | Predicate p [CTerm v f]+    | Equal (CTerm v f) (CTerm v f)+    deriving (Eq, Ord, Data, Typeable)++data CTerm v f+    = Function f [CTerm v f]+    | Variable v+    deriving (Eq, Ord, Data, Typeable)++data Connective+    = Imply+    | Equiv+    | And+    | Or+    deriving (Eq, Ord, Show, Data, Typeable)++data Quantifier+    = ForAll+    | ExistsCh+    deriving (Eq, Ord, Show, Data, Typeable)++instance Negatable (Sentence v p f) where+    negatePrivate = Not+    foldNegation normal inverted (Not x) = foldNegation inverted normal x+    foldNegation normal _ x = normal x++instance (Constants p, Eq (Sentence v p f)) => Constants (Sentence v p f) where+    fromBool x = Predicate (fromBool x) []+    asBool x+        | fromBool True == x = Just True+        | fromBool False == x = Just False+        | True = Nothing++instance ({- Constants (Sentence v p f), -} Ord v, Ord p, Ord f) => Combinable (Sentence v p f) where+    x .<=>. y = Connective x Equiv y+    x .=>.  y = Connective x Imply y+    x .|.   y = Connective x Or y+    x .&.   y = Connective x And y++instance (Predicate p, Function f v) => Formula (Sentence v p f) (Sentence v p f) where+    atomic (Connective _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic (Quantifier _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic (Not _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic x@(Predicate _ _) = x+    atomic x@(Equal _ _) = x+    foldAtoms = foldAtomsFirstOrder+    mapAtoms = mapAtomsFirstOrder++instance (Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v, Combinable (Sentence v p f)) =>+         PropositionalFormula (Sentence v p f) (Sentence v p f) where+    foldPropositional co tf at formula =+        case formula of+          Not x -> co ((:~:) x)+          Quantifier _ _ _ -> error "Logic.Instance.Chiou.foldF0: unexpected"+          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)+          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)+          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)+          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)+          Predicate p ts -> maybe (at (Predicate p ts)) tf (asBool p)+          Equal t1 t2 -> at (Equal t1 t2)++data AtomicFunction v+    = AtomicFunction String+    -- This is redundant with the SkolemFunction and SkolemConstant+    -- constructors in the Chiou Term type.+    | AtomicSkolemFunction v+    deriving (Eq, Show)++instance IsString (AtomicFunction v) where+    fromString = AtomicFunction++instance Variable v => Skolem (AtomicFunction v) v where+    toSkolem = AtomicSkolemFunction+    isSkolem (AtomicSkolemFunction _) = True+    isSkolem _ = False++-- The Atom type is not cleanly distinguished from the Sentence type, so we need an Atom instance for Sentence.+instance (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) where+    foldApply ap tf (Predicate p ts) = maybe (ap p ts) tf (asBool p)+    foldApply _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"+    apply' = Predicate++instance Predicate p => AtomEq (Sentence v p f) p (CTerm v f) where+    foldAtomEq ap tf _ (Predicate p ts) = if p == true then tf True else if p == false then tf False else ap p ts+    foldAtomEq _ _ eq (Equal t1 t2) = eq t1 t2+    foldAtomEq _ _ _ _ = error "Data.Logic.Instances.Chiou: Invalid atom"+    equals = Equal+    applyEq' = Predicate++instance (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f) where+    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0++instance (Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f) where+    fixity = fixityFirstOrder++instance (Formula (Sentence v p f) (Sentence v p f),+          Variable v, Predicate p, Function f v) =>+          FirstOrderFormula (Sentence v p f) (Sentence v p f) v where+    for_all v x = Quantifier ForAll [v] x+    exists v x = Quantifier ExistsCh [v] x+    foldFirstOrder qu co tf at f =+        case f of+          Not x -> co ((:~:) x)+          Quantifier op (v:vs) f' ->+              let op' = case op of+                          ForAll -> Forall+                          ExistsCh -> Exists in+              -- Use Logic.quant' here instead of the constructor+              -- Quantifier so as not to create quantifications with+              -- empty variable lists.+              qu op' v (quant' op' vs f')+          Quantifier _ [] f' -> foldFirstOrder qu co tf at f'+          Connective f1 Imply f2 -> co (BinOp f1 (:=>:) f2)+          Connective f1 Equiv f2 -> co (BinOp f1 (:<=>:) f2)+          Connective f1 And f2 -> co (BinOp f1 (:&:) f2)+          Connective f1 Or f2 -> co (BinOp f1 (:|:) f2)+          Predicate _ _ -> at f+          Equal _ _ -> at f+{-+    zipFirstOrder qu co tf at f1 f2 =+        case (f1, f2) of+          (Not f1', Not f2') -> co ((:~:) f1') ((:~:) f2')+          (Quantifier op1 (v1:vs1) f1', Quantifier op2 (v2:vs2) f2') ->+              if op1 == op2+              then let op' = case op1 of+                               ForAll -> Forall+                               ExistsCh -> Exists in+                   qu op' v1 (Quantifier op1 vs1 f1') Forall v2 (Quantifier op2 vs2 f2')+              else Nothing+          (Quantifier q1 [] f1', Quantifier q2 [] f2') ->+              if q1 == q2 then zipFirstOrder qu co tf at f1' f2' else Nothing+          (Connective l1 op1 r1, Connective l2 op2 r2) ->+              case (op1, op2) of+                (And, And) -> co (BinOp l1 (:&:) r1) (BinOp l2 (:&:) r2)+                (Or, Or) -> co (BinOp l1 (:|:) r1) (BinOp l2 (:|:) r2)+                (Imply, Imply) -> co (BinOp l1 (:=>:) r1) (BinOp l2 (:=>:) r2)+                (Equiv, Equiv) -> co (BinOp l1 (:<=>:) r1) (BinOp l2 (:<=>:) r2)+                _ -> Nothing+          (Equal _ _, Equal _ _) -> at f1 f2+          (Predicate _ _, Predicate _ _) -> at f1 f2+          _ -> Nothing+-}++instance (Variable v, Function f v) => Term (CTerm v f) v f where+    foldTerm v fn t =+        case t of+          Variable x -> v x+          Function f ts -> fn f ts+    zipTerms  v f t1 t2 =+        case (t1, t2) of+          (Variable v1, Variable v2) -> v v1 v2+          (Function f1 ts1, Function f2 ts2) -> f f1 ts1 f2 ts2+          _ -> Nothing+    vt = Variable+    fApp f ts = Function f ts++data ConjunctiveNormalForm v p f =+    CNF [Sentence v p f]+    deriving (Eq)++data NormalSentence v p f+    = NFNot (NormalSentence v p f)+    | NFPredicate p [NormalTerm v f]+    | NFEqual (NormalTerm v f) (NormalTerm v f)+    deriving (Eq, Ord, Data, Typeable)++-- We need a distinct type here because of the functional dependencies+-- in class FirstOrderFormula.+data NormalTerm v f+    = NormalFunction f [NormalTerm v f]+    | NormalVariable v+    deriving (Eq, Ord, Data, Typeable)++instance (Constants p, Eq (NormalSentence v p f)) => Constants (NormalSentence v p f) where+    fromBool x = NFPredicate (fromBool x) []+    asBool x+        | fromBool True == x = Just True+        | fromBool False == x = Just False+        | True = Nothing++instance Negatable (NormalSentence v p f) where+    negatePrivate = NFNot+    foldNegation normal inverted (NFNot x) = foldNegation inverted normal x+    foldNegation normal _ x = normal x++{-+instance (Arity p, Constants p, Combinable (NormalSentence v p f)) => Pred p (NormalTerm v f) (NormalSentence v p f) where+    pApp0 x = NFPredicate x []+    pApp1 x a = NFPredicate x [a]+    pApp2 x a b = NFPredicate x [a,b]+    pApp3 x a b c = NFPredicate x [a,b,c]+    pApp4 x a b c d = NFPredicate x [a,b,c,d]+    pApp5 x a b c d e = NFPredicate x [a,b,c,d,e]+    pApp6 x a b c d e f = NFPredicate x [a,b,c,d,e,f]+    pApp7 x a b c d e f g = NFPredicate x [a,b,c,d,e,f,g]+    x .=. y = NFEqual x y+    x .!=. y = NFNot (NFEqual x y)+-}++instance (Formula (NormalSentence v p f) (NormalSentence v p f),+          Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f) where+    pretty = prettyFirstOrder (\ _ a -> pretty a) pretty 0++instance (Predicate p, Function f v, Combinable (NormalSentence v p f)) => Formula (NormalSentence v p f) (NormalSentence v p f) where+    atomic x@(NFPredicate _ _) = x+    atomic x@(NFEqual _ _) = x+    atomic _ = error "Chiou: atomic"+    foldAtoms = foldAtomsFirstOrder+    mapAtoms = mapAtomsFirstOrder++instance (Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Term (NormalTerm v f) v f,+          Variable v, Predicate p, Function f v) => FirstOrderFormula (NormalSentence v p f) (NormalSentence v p f) v where+    for_all _ _ = error "FirstOrderFormula NormalSentence"+    exists _ _ = error "FirstOrderFormula NormalSentence"+    foldFirstOrder _ co tf at f =+        case f of+          NFNot x -> co ((:~:) x)+          NFEqual _ _ -> at f+          NFPredicate p _ -> maybe (at f) tf (asBool p)+{-+    zipFirstOrder _ co tf at f1 f2 =+        case (f1, f2) of+          (NFNot f1', NFNot f2') -> co ((:~:) f1') ((:~:) f2')+          (NFEqual _ _, NFEqual _ _) -> at f1 f2+          (NFPredicate _ _, NFPredicate _ _) -> at f1 f2+          _ -> Nothing+-}++instance (Formula (NormalSentence v p f) (NormalSentence v p f),+          Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f) where+    fixity = fixityFirstOrder++instance (Variable v, Function f v) => Term (NormalTerm v f) v f where+    vt = NormalVariable+    fApp = NormalFunction+    foldTerm v f t =+            case t of+              NormalVariable x -> v x+              NormalFunction x ts -> f x ts+    zipTerms v fn t1 t2 =+        case (t1, t2) of+          (NormalVariable x1, NormalVariable x2) -> v x1 x2+          (NormalFunction f1 ts1, NormalFunction f2 ts2) -> fn f1 ts1 f2 ts2+          _ -> Nothing++toSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Atom (Sentence v p f) (CTerm v f) v, Function f v, Variable v, Predicate p) =>+              NormalSentence v p f -> Sentence v p f+toSentence (NFNot s) = (.~.) (toSentence s)+toSentence (NFEqual t1 t2) = toTerm t1 .=. toTerm t2+toSentence (NFPredicate p ts) = pApp p (map toTerm ts)++toTerm :: (Variable v, Function f v) => NormalTerm v f -> CTerm v f+toTerm (NormalFunction f ts) = fApp f (map toTerm ts)+toTerm (NormalVariable v) = vt v++fromSentence :: forall v p f. (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Predicate p) =>+                Sentence v p f -> NormalSentence v p f+fromSentence = foldFirstOrder +                 (\ _ _ _ -> error "fromSentence 1")+                 (\ cm ->+                      case cm of+                        ((:~:) f) -> NFNot (fromSentence f)+                        _ -> error "fromSentence 2")+                 (\ x -> NFPredicate (fromBool x) [])+                 (foldAtomEq (\ p ts -> NFPredicate p (map fromTerm ts))+                             (\ x -> NFPredicate (fromBool x) [])+                             (\ t1 t2 -> NFEqual (fromTerm t1) (fromTerm t2)))++fromTerm :: CTerm v f -> NormalTerm v f+fromTerm (Function f ts) = NormalFunction f (map fromTerm ts)+fromTerm (Variable v) = NormalVariable v
Data/Logic/Instances/SatSolver.hs view
@@ -37,7 +37,7 @@ instance ClauseNormalFormula CNF Literal where     clauses = S.fromList . map S.fromList     makeCNF = map S.toList . S.toList-    satisfiable cnf = return . not . null $ assertTrue' cnf newSatSolver >>= solve+    satisfiable cnf = return . not . (null :: [a] -> Bool) $ assertTrue' cnf newSatSolver >>= solve  toCNF :: (Monad m,           FirstOrderFormula formula atom v,
− Data/Logic/Tests/Chiou0.hs 
@@ -1,102 +0,0 @@-{-# LANGUAGE OverloadedStrings, StandaloneDeriving #-}-{-# OPTIONS -fno-warn-orphans #-}--module Data.Logic.Tests.Chiou0 where--import Control.Monad.Trans (MonadIO, liftIO)-import Data.Logic.Classes.Combine (Combinable(..))-import Data.Logic.Classes.Equals (pApp)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))-import Data.Logic.Classes.Negate (Negatable(..), (.~.))-import Data.Logic.Classes.Skolem (Skolem(..))-import Data.Logic.Classes.Term (Term(..))-import Data.Logic.Harrison.Skolem (SkolemT)-import Data.Logic.KnowledgeBase (ProverT, runProver', Proof(..), ProofResult(..), loadKB, theoremKB {-, askKB, showKB-})-import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')-import Data.Logic.Resolution (SetOfSupport)-import Data.Logic.Tests.Common (V(..), AtomicFunction(..), TFormula, TTerm, myTest)-import Data.Map (fromList)-import qualified Data.Set as S-import Test.HUnit--tests :: Test-tests = TestLabel "Test.Chiou0" $ TestList [loadTest, proofTest1, proofTest2]--loadTest :: Test-loadTest =-    myTest "Chiuo0 - loadKB test" expected (runProver' Nothing (loadKB sentences))-    where-      expected :: [Proof TFormula]-      expected = [Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem "x") []])]),-                                             makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])])]),-                  Proof Invalid (S.fromList [makeINF' ([(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [vt ("x"),vt ("y")])]) ([(pApp ("AnimalLover") [vt ("x")])])]),-                  Proof Invalid (S.fromList [makeINF' ([(pApp ("Animal") [vt ("y")]),(pApp ("AnimalLover") [vt ("x")]),(pApp ("Kills") [vt ("x"),vt ("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") [vt ("x")])]) ([(pApp ("Animal") [vt ("x")])])])]--proofTest1 :: Test-proofTest1 = myTest "Chiuo0 - proof test 1" proof1 (runProver' Nothing (loadKB sentences >> theoremKB (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula)))--inf' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit-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") [vt ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),-            (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),-            (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),-            (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),-            (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []])]) ([]),fromList []),-            (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),-            (makeINF' ([(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),-            (makeINF' ([(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList [])]))--proofTest2 :: Test-proofTest2 = myTest "Chiuo0 - proof test 2" proof2 (runProver' Nothing (loadKB sentences >> theoremKB conjecture))-    where-      conjecture :: TFormula-      conjecture = (pApp "Kills" [fApp "Curiosity" [], fApp (Fn "Tuna") []])--proof2 :: (Bool, SetOfSupport TFormula V TTerm)-proof2 = (True,-          S.fromList-          [(makeINF' ([]) ([]),fromList []),-           (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),-           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),-           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),-           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y2")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],vt ("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") [vt ("y2")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Dog") [vt ("y2")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-           (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])--testProof :: MonadIO m => String -> (TFormula, Bool, (S.Set (ImplicativeForm TFormula))) -> ProverT (ImplicativeForm TFormula) (SkolemT 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) (SkolemT V TTerm m) [Proof TFormula]-loadCmd = loadKB sentences--sentences :: [TFormula]-sentences = [exists "x" ((pApp "Dog" [vt "x"]) .&. (pApp "Owns" [fApp "Jack" [], vt "x"])),-             for_all "x" (((exists "y" (pApp "Dog" [vt "y"])) .&. (pApp "Owns" [vt "x", vt "y"])) .=>. (pApp "AnimalLover" [vt "x"])),-             for_all "x" ((pApp "AnimalLover" [vt "x"]) .=>. (for_all "y" ((pApp "Animal" [vt "y"]) .=>. ((.~.) (pApp "Kills" [vt "x", vt "y"]))))),-             (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []]) .|. (pApp "Kills" [fApp "Curiosity" [], fApp "Tuna" []]),-             pApp "Cat" [fApp "Tuna" []],-             for_all "x" ((pApp "Cat" [vt "x"]) .=>. (pApp "Animal" [vt "x"]))]
− Data/Logic/Tests/Common.hs 
@@ -1,325 +0,0 @@--- |Types to use for creating test cases.  These are used in the Logic--- package test cases, and are exported for use in its clients.-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes,-             ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeSynonymInstances, UndecidableInstances #-}-{-# OPTIONS -Wwarn #-}-module Data.Logic.Tests.Common-    ( render-    , myTest-      -- * Formula parameter types-    , V(..)-    , Pr(..)-    , AtomicFunction(..)-    , TFormula-    , TAtom-    , TTerm-    , TTestFormula-    , prettyV-    , prettyP-    , prettyF-      -- * Test case types-    , TestFormula(..)-    , Expected(..)-    , doTest-    , TestProof(..)-    , TTestProof-    , ProofExpected(..)-    , doProof-    ) where--import Control.Monad.Reader (MonadPlus(..), msum)-import Data.Boolean.SatSolver (CNF)-import Data.Char (isDigit)-import Data.Generics (Data, Typeable, listify)-import Data.Logic.Classes.Apply (Predicate)-import Data.Logic.Classes.Arity (Arity(arity))-import Data.Logic.Classes.ClauseNormalForm (ClauseNormalFormula(satisfiable))-import Data.Logic.Classes.Constants (Constants(..), prettyBool)-import Data.Logic.Classes.Equals (AtomEq)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula, convertFOF, prettyFirstOrder)-import Data.Logic.Classes.Literal (Literal)-import Data.Logic.Classes.Pretty (Pretty(pretty))-import Data.Logic.Classes.Propositional (PropositionalFormula)-import qualified Data.Logic.Classes.Skolem as C-import Data.Logic.Classes.Term (Term(vt, fApp, foldTerm), Function)-import Data.Logic.Classes.Variable (Variable(..))-import Data.Logic.Harrison.Normal (trivial)-import Data.Logic.Harrison.Skolem (Skolem, skolemize, runSkolem, pnf, nnf, simplify)-import qualified Data.Logic.Instances.Chiou as Ch-import Data.Logic.Instances.PropLogic (plSat)-import qualified Data.Logic.Instances.SatSolver as SS-import Data.Logic.KnowledgeBase (WithId, runProver', Proof, loadKB, theoremKB, getKB)-import Data.Logic.Normal.Clause (clauseNormalForm)-import Data.Logic.Normal.Implicative (ImplicativeForm, runNormal, runNormalT)-import Data.Logic.Resolution (SetOfSupport)-import qualified Data.Logic.Types.FirstOrder as P-import qualified Data.Set as S-import Data.String (IsString(fromString))-import Text.PrettyPrint (Style(mode), renderStyle, style, Mode(OneLineMode), (<>))----import PropLogic (PropForm)--import Test.HUnit-import Text.PrettyPrint (Doc, text)---- | Render a Pretty instance in single line mode-render :: Pretty a => a -> String-render = renderStyle (style {mode = OneLineMode}) . pretty--myTest :: (Show a, Eq a) => String -> a -> a -> Test-myTest label expected input =-    TestLabel label $ TestCase (assertEqual label expected input)--newtype V = V String deriving (Eq, Ord, Data, Typeable)--instance IsString V where-    fromString = V--instance Show V where-    show (V s) = show s--prettyV :: V -> Doc-prettyV (V s) = text s--instance Pretty V where-    pretty = prettyV--instance Variable V where-    prefix p (V s) = V (p ++ s)-    variant x@(V s) xs = if S.member x xs then variant (V (next s)) xs else x-    prettyVariable (V s) = text s--next :: String -> String-next s =-    case break (not . isDigit) (reverse s) of-      (_, "") -> "x"-      ("", nondigits) -> nondigits ++ "2"-      (digits, nondigits) -> nondigits ++ show (1 + read (reverse digits) :: Int)---- |A newtype for the Primitive Predicate parameter.-data Pr-    = Pr String-    | T-    | F-    | Equals-    deriving (Eq, Ord, Data, Typeable)--instance Predicate Pr--instance IsString Pr where-    fromString = Pr--instance Constants Pr where-    fromBool True = T-    fromBool False = F-    asBool T = Just True-    asBool F = Just False-    asBool _ = Nothing--instance Arity Pr where-    arity (Pr _) = Nothing-    arity T = Just 0-    arity F = Just 0-    arity Equals = Just 2--instance Show Pr where-    show T = "fromBool True"-    show F = "fromBool False"-    show Equals = ".=."-    show (Pr s) = show s            -- Because Pr is an instance of IsString--prettyP :: Pr -> Doc-prettyP T = prettyBool True-prettyP F = prettyBool False-prettyP Equals = text ".=."-prettyP (Pr s) = text s--instance Pretty Pr where-    pretty = prettyP--data AtomicFunction-    = Fn String-    | Skolem V-    deriving (Eq, Ord, Data, Typeable)--instance Function AtomicFunction V--instance C.Skolem AtomicFunction V where-    toSkolem = Skolem-    isSkolem (Skolem _) = True-    isSkolem _ = False--instance IsString AtomicFunction where-    fromString = Fn--instance Show AtomicFunction where-    show (Fn s) = show s-    show (Skolem v) = "(toSkolem " ++ show v ++ ")"--prettyF :: AtomicFunction -> Doc-prettyF (Fn s) = text s-prettyF (Skolem v) = text "sK" <> pretty v--instance Pretty AtomicFunction where-    pretty = prettyF--type TFormula = P.Formula V Pr AtomicFunction-type TAtom = P.Predicate Pr TTerm-type TTerm = P.PTerm V AtomicFunction--{--instance Pretty TFormula where-    pretty = prettyFirstOrder (const pretty) pretty 0--}---- |This allows you to use an expression that returns the Doc type in a--- unit test, such as prettyFirstOrder.-instance Eq Doc where-    a == b = show a == show b--data TestFormula formula atom v-    = TestFormula-      { formula :: formula-      , name :: String-      , expected :: [Expected formula atom v]-      } -- deriving (Data, Typeable)---- |Some values that we might expect after transforming the formula.-data Expected formula atom v-    = FirstOrderFormula formula-    | SimplifiedForm formula-    | NegationNormalForm formula-    | PrenexNormalForm formula-    | SkolemNormalForm formula-    | SkolemNumbers (S.Set AtomicFunction)-    | ClauseNormalForm (S.Set (S.Set formula))-    | TrivialClauses [(Bool, (S.Set formula))]-    | ConvertToChiou (Ch.Sentence V Pr AtomicFunction)-    | ChiouKB1 (Proof formula)-    | PropLogicSat Bool-    | SatSolverCNF CNF-    | SatSolverSat Bool-    -- deriving (Data, Typeable)--deriving instance Show (Ch.Sentence V Pr AtomicFunction)-deriving instance Show (Ch.CTerm V AtomicFunction)--type TTestFormula = TestFormula TFormula TAtom V--doTest :: TTestFormula -> Test-doTest f =-    TestLabel (name f) $ TestList $ -    map doExpected (expected f)-    where-      doExpected (FirstOrderFormula f') =-          myTest (name f ++ " original formula") (p f') (p (formula f))-      doExpected (SimplifiedForm f') =-          myTest (name f ++ " simplified") (p f') (p (simplify (formula f)))-      doExpected (PrenexNormalForm f') =-          myTest (name f ++ " prenex normal form") (p f') (p (pnf (formula f)))-      doExpected (NegationNormalForm f') =-          myTest (name f ++ " negation normal form") (p f') (p (nnf . simplify $ (formula f)))-      doExpected (SkolemNormalForm f') =-          myTest (name f ++ " skolem normal form") (p f') (p (runSkolem (skolemize id (formula f) :: Skolem V (P.PTerm V AtomicFunction) TFormula)))-      doExpected (SkolemNumbers f') =-          myTest (name f ++ " skolem numbers") f' (skolemSet (runSkolem (skolemize id (formula f) :: Skolem V (P.PTerm V AtomicFunction) TFormula)))-      doExpected (ClauseNormalForm fss) =-          myTest (name f ++ " clause normal form") fss (S.map (S.map p) (runSkolem (clauseNormalForm (formula f))))-      doExpected (TrivialClauses flags) =-          myTest (name f ++ " trivial clauses") flags (map (\ (x :: S.Set TFormula) -> (trivial x, x)) (S.toList (runSkolem (clauseNormalForm (formula f :: TFormula)))))-      doExpected (ConvertToChiou result) =-          -- We need to convert (formula f) to Chiou and see if it matches result.-          let ca :: TAtom -> Ch.Sentence V Pr AtomicFunction-              -- ca = undefined-              ca (P.Apply p ts) = Ch.Predicate p (map ct ts)-              ca (P.Equal t1 t2) = Ch.Equal (ct t1) (ct t2)-              ct :: TTerm -> Ch.CTerm V AtomicFunction-              ct = foldTerm cv fn-              cv :: V -> Ch.CTerm V AtomicFunction-              cv = vt-              fn :: AtomicFunction -> [TTerm] -> Ch.CTerm V AtomicFunction-              fn f ts = fApp f (map ct ts) in-          myTest (name f ++ " converted to Chiou") result (convertFOF ca id (formula f) :: Ch.Sentence V Pr AtomicFunction)-      doExpected (ChiouKB1 result) =-          myTest (name f ++ " Chiou KB") result (runProver' Nothing (loadKB [formula f] >>= return . head))-      doExpected (PropLogicSat result) =-          myTest (name f ++ " PropLogic.satisfiable") result (runSkolem (plSat (formula f)))-      doExpected (SatSolverCNF result) =-          myTest (name f ++ " SatSolver CNF") (norm result) (runNormal (SS.toCNF (formula f)))-      doExpected (SatSolverSat result) =-          myTest (name f ++ " SatSolver CNF") result (null (runNormalT (SS.toCNF (formula f) >>= satisfiable)))-      p = id--      norm = map S.toList . S.toList . S.fromList . map S.fromList--{--skolemNormalForm' f = (skolem' . nnf . simplify $ f) >>= return . prenex' . nnf' . simplify'---- skolem' :: formula -> SkolemT v term m pf-skolem' :: ( Monad m-           , Variable v-           , Term term v f-           , FirstOrderFormula formula atom v-           -- , Atom atom term v-           -- , PropositionalFormula pf atom-           -- , Formula formula term v-           ) =>-           formula -> SkolemT v term m pf-skolem' = undefined--}--skolemSet :: forall formula atom term v p f. (FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Data formula) => formula -> S.Set f-skolemSet =-    foldr ins S.empty . skolemList-    where-      ins :: f -> S.Set f -> S.Set f-      ins f s = if C.isSkolem f-                then S.insert f s-                else s-      skolemList :: (FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Data f, Typeable f, Data formula) => formula -> [f]-      skolemList inf = gFind inf :: (Typeable f => [f])---- | @gFind a@ will extract any elements of type @b@ from--- @a@'s structure in accordance with the MonadPlus--- instance, e.g. Maybe Foo will return the first Foo--- found while [Foo] will return the list of Foos found.-gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b-gFind = msum . map return . listify (const True)--data TestProof formula term v-    = TestProof-      { proofName :: String-      , proofKnowledge :: (String, [formula])-      , conjecture :: formula-      , proofExpected :: [ProofExpected formula v term]-      } deriving (Data, Typeable)--type TTestProof = TestProof TFormula TTerm V--data ProofExpected formula v term-    = ChiouResult (Bool, SetOfSupport formula v term)-    | ChiouKB (S.Set (WithId (ImplicativeForm formula)))-    deriving (Data, Typeable)--doProof :: forall formula atom term v p f. (FirstOrderFormula formula atom v,-                                            PropositionalFormula formula atom,-                                            AtomEq atom p term, atom ~ P.Predicate p (P.PTerm v f),-                                            Term term v f, term ~ P.PTerm v f,-                                            Literal formula atom,-                                            Ord formula, Data formula, Eq term, Show term, Show v, Show formula, Constants p, Eq p, Ord f, Show f) =>-           TestProof formula term v -> Test-doProof p =-    TestLabel (proofName p) $ TestList $-    concatMap doExpected (proofExpected p)-    where-      doExpected :: ProofExpected formula v term -> [Test]-      doExpected (ChiouResult result) =-          [myTest (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " using Chiou prover")-                  result-                  (runProver' Nothing (loadKB kb >> theoremKB c))]-      doExpected (ChiouKB result) =-          [myTest (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " Chiou knowledge base")-                  result-                  (runProver' Nothing (loadKB kb >> getKB))]-      kb = snd (proofKnowledge p) :: [formula]-      c = conjecture p :: formula
− Data/Logic/Tests/Data.hs 
@@ -1,1064 +0,0 @@-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies  #-}-{-# OPTIONS -fno-warn-name-shadowing #-}-module Data.Logic.Tests.Data-    ( tests-    , allFormulas-    , proofs-{--    , formulas-    , animalKB-    , animalConjectures-    , chang43KB-    , chang43Conjecture-    , chang43ConjectureRenamed--}-    ) where--import Data.Boolean.SatSolver (Literal(..))---import Data.Generics (Data, Typeable)-import Data.Logic.Classes.Combine (Combinable(..))-import Data.Logic.Classes.Constants (Constants(..))-import Data.Logic.Classes.Equals (AtomEq, (.=.), pApp, pApp2)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), for_all', exists')-import Data.Logic.Classes.Negate ((.~.))-import Data.Logic.Classes.Term (Term(..))-import Data.Logic.Classes.Skolem (Skolem(toSkolem))---import Data.Logic.Classes.Negate (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.Tests.Common (TestFormula(..), TestProof(..), Expected(..), ProofExpected(..), doTest, doProof,-                                TFormula, TAtom, TTerm, V, Pr, AtomicFunction, TTestFormula, TTestProof)---import Data.Logic.Types.FirstOrder (Predicate(..), PTerm(..))-import Data.Map (fromList)-import qualified Data.Set as S-import Data.String (IsString)-import Test.HUnit--{--:m +Data.Logic.Test-:m +Data.Logic.Types.FirstOrder-:m +Data.Set-runNormal (clauseNormalForm (true :: Formula V Pr AtomicFunction)) :: Set (Set (Formula V Pr AtomicFunction))-runNormal (skolemNormalForm (true :: Formula V Pr AtomicFunction)) :: Formula V Pr AtomicFunction-:m +Data.Logic.Normal.Prenex-prenexNormalForm true :: Formula V Pr AtomicFunction-:m +Data.Logic.Normal.Skolem-:m +Data.Logic.Normal.Negation--}--tests :: [TTestFormula] -> [TTestProof] -> Test-tests fs ps =-    TestLabel "Test.Data" $ TestList (map doTest fs ++ map doProof ps)--allFormulas :: [TTestFormula]-allFormulas = (formulas ++-               concatMap snd [animalKB, chang43KB] ++-               animalConjectures ++-               [chang43Conjecture, chang43ConjectureRenamed])--formulas :: [TTestFormula]-formulas =-    let n = (.~.)-        p = pApp "p"-        q = pApp "q"-        r = pApp "r"-        s = pApp "s"-        t = pApp "t"-        p0 = p []-        q0 = q []-        r0 = r []-        s0 = s []-        t0 = t []-        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm)-        z2 = vt "z2" :: TTerm 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" [vt "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 [z2,x])) .&.-                                (((.~.) (f [z2,y]))))) .|.-                              (((((.~.) (f [z2,x]))) .&.-                                ((f [z2,y])))))))))))))-                   , ClauseNormalForm -                     (toSS [[(pApp2 ("f") (vt ("z")) (vt ("x"))),-                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y"))))],-                            [(pApp2 ("f") (vt ("z")) (vt ("x"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],-                            [(pApp2 ("f") (vt ("z")) (vt ("x"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),-                             ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],-                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x"))))],-                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],-                            [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                             ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),-                             ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],-                            [(pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                             (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),-                             (pApp2 ("q") (vt ("x")) (vt ("y")))],-                            [(pApp2 ("q") (vt ("x")) (vt ("y"))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                             ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))]])-                   ]-      }-    , TestFormula-      { name = "move quantifiers out"-      , formula = (for_all "x" (pApp "p" [x]) .&. (pApp "q" [x]))-      , expected = [PrenexNormalForm (for_all "x2" ((pApp "p" [vt ("x2")]) .&. ((pApp "q" [vt ("x")]))))]-      }-    , TestFormula-      { name = "skolemize2"-      , formula = exists "x" (for_all "y" (pApp "loves" [x, y]))-      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x") [],y])]-      }-    , TestFormula-      { name = "skolemize3"-      , formula = for_all "y" (exists "x" (pApp "loves" [x, y]))-      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x") [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 "x") [],-                                                 vt ("y"),-                                                 vt ("z"),-                                                 fApp (toSkolem "u") [vt ("y"),vt ("z")],-                                                 vt ("v"),-                                                 fApp (toSkolem "w") [vt ("v"), vt ("y"),vt ("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") [vt ("x"),vt ("y")])) .&.-                       ((pApp ("Q") [vt ("x"),vt ("z")]))) .|.-                      ((pApp ("R") [vt ("x"),vt ("y"),vt ("z")])))-                   , ClauseNormalForm-                     (toSS -                      [[((.~.) (pApp ("P") [vt ("x"),vt ("y")])),-                       (pApp ("R") [vt ("x"),vt ("y"),vt ("z")])],-                      [(pApp ("Q") [vt ("x"),vt ("z")]),-                       (pApp ("R") [vt ("x"),vt ("y"),vt ("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 "x") [x,x,y,z],y]-          sk2 = f [fApp (toSkolem "x") [x,x,y,z],x] 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 = vt "x" :: TTerm-          y = vt "y" :: TTerm-          x' = vt "x" :: C.CTerm V AtomicFunction-          y' = vt "y" :: C.CTerm V AtomicFunction in-      TestFormula-      { name = "convert to Chiou 1"-      , formula = exists "x" (x .=. y)-      , expected = [ConvertToChiou (exists "x" (x' .=. y') :: C.Sentence V Pr AtomicFunction)]-      }-    , let s = pApp "s"-          s' = pApp "s"-          x' = vt "x"-          y' = vt "y" in-      TestFormula-      { name = "convert to Chiou 2"-      , formula = s [fApp ("a") [x, y]]-      , expected = [ConvertToChiou (s' [fApp "a" [x', y']])]-      }-    , let s = pApp "s"-          h = pApp "h"-          m = pApp "m"-          s' = pApp "s"-          h' = pApp "h"-          m' = pApp "m"-          x' = vt "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 a b = pApp "taller" [a, b]-          wise a = pApp "wise" [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") [vt ("y")]),-                       ((.~.) (pApp ("taller") [vt ("y"),fApp (toSkolem "x") [vt ("y")]]))],-                      [(pApp ("wise") [vt ("y")]),-                       ((.~.) (pApp ("wise") [fApp (toSkolem "x") [vt ("y")]]))]])]-      }-    , TestFormula-      { name = "cnf test 2"-      , formula = ((.~.) (exists "x" (pApp "s" [x] .&. pApp "q" [x])))-      , expected = [ ClauseNormalForm (toSS -                                       [[((.~.) (pApp ("q") [vt ("x")])),-                                         ((.~.) (pApp ("s") [vt ("x")]))]])-                   , PrenexNormalForm (for_all "x"-                                       (((.~.) (pApp ("s") [vt ("x")])) .|.-                                        (((.~.) (pApp ("q") [vt ("x")])))))-                                     {- [[((.~.) (pApp "s" [vt "x"])),-                                        ((.~.) (pApp "q" [vt "x"]))]] -}-                   ]-      }-    , TestFormula-      { name = "cnf test 3"-      , formula = (for_all "x" (p [x] .=>. (q [x] .|. r [x])))-      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [vt "x"])),(pApp "q" [vt "x"]),(pApp "r" [vt "x"])]])]-      }-    , TestFormula-      { name = "cnf test 4"-      , formula = ((.~.) (exists "x" (p [x] .=>. exists "y" (q [y]))))-      , expected = [ClauseNormalForm (toSS [[(pApp "p" [vt "x"])],[((.~.) (pApp "q" [vt "y"]))]])]-      }-    , TestFormula-      { name = "cnf test 5"-      , formula = (for_all "x" (q [x] .|. r [x] .=>. s [x]))-      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "q" [vt "x"])),(pApp "s" [vt "x"])],[((.~.) (pApp "r" [vt "x"])),(pApp "s" [vt "x"])]])]-      }-    , TestFormula-      { name = "cnf test 6"-      , formula = (exists "x" (p0 .=>. pApp "f" [x]))-      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [])),(pApp "f" [fApp (toSkolem "x") []])]])]-      }-    , let p = pApp "p" []-          f' = pApp "f" [x]-          f = pApp "f" [fApp (toSkolem "x") []] 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 "x") []])]),-                                     (False,S.fromList [((.~.) (pApp ("f") [fApp (toSkolem "x") []])),(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" [vt "x",fApp (toSkolem "y") [vt "z"]])),(pApp "f" [vt "x",vt "z"])],-                           [((.~.) (pApp "f" [vt "x",fApp (toSkolem "y") [vt "z"]])),((.~.) (pApp "f" [vt "x",vt "x"]))],-                           [((.~.) (pApp "f" [vt "x",vt "z"])),(pApp "f" [vt "x",vt "x"]),(pApp "f" [vt "x",fApp (toSkolem "y") [vt "z"]])]])]-      }-    , let f = pApp "f" -          q = pApp "q"-          (x, y, z) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm) 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-                     [[(pApp2 ("f") (vt ("z")) (vt ("x"))),-                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),-                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y"))))],-                      [(pApp2 ("f") (vt ("z")) (vt ("x"))),-                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],-                      [(pApp2 ("f") (vt ("z")) (vt ("x"))),-                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("y")))),-                       ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],-                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),((.~.) (pApp2 ("f") (vt ("z")) (vt ("x"))))],-                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))))],-                      [(pApp2 ("f") (vt ("z")) (vt ("y"))),-                       ((.~.) (pApp2 ("f") (vt ("z")) (vt ("x")))),-                       ((.~.) (pApp2 ("q") (vt ("x")) (vt ("y"))))],-                      [(pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x"))),-                       (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("y"))),-                       (pApp2 ("q") (vt ("x")) (vt ("y")))],-                      [(pApp2 ("q") (vt ("x")) (vt ("y"))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("x")))),-                       ((.~.) (pApp2 ("f") (fApp (toSkolem "z") [vt ("x"),vt ("y")]) (vt ("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") [vt ("x"),fApp (toSkolem "y") [vt ("x")]]),-                       (pApp ("q") [fApp (toSkolem "y") [vt "x"],fApp (toSkolem "x2") [vt "x"],fApp (toSkolem "z") [vt "x"]])],-                      [(pApp ("p") [vt ("x"),fApp (toSkolem "y") [vt ("x")]]),-                       ((.~.) (pApp ("r") [fApp (toSkolem "y") [vt "x"]]))]])-                   ]-      }-    , 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" [vt "x",vt "z"])),((.~.) (pApp "q" [vt "x",fApp (toSkolem "y") [vt "x",vt "z"]]))],-                     [((.~.) (pApp "p" [vt "x",vt "z"])),(pApp "r" [fApp (toSkolem "y") [vt "x",vt "z"],vt "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" [vt "x"] .|. (pApp "p" [vt "y"] .&. false))) .=>.-                   (exists "z" q))-      , expected = [ SimplifiedForm ((for_all "x" (pApp "p" [vt "x"])) .=>.-                                        (pApp "q" [])) ] }-    , TestFormula-      { name = "nnf 141.1"-      , formula = ((for_all "x" (pApp "p" [vt "x"])) .=>. ((exists "y" (pApp "q" [vt "y"])) .<=>. (exists "z" (pApp "p" [vt "z"] .&. pApp "q" [vt "z"]))))-      , expected = [ NegationNormalForm -                     ((exists "x" ((.~.) (pApp "p" [vt "x"]))) .|.-                      ((((exists "y" (pApp "q" [vt "y"])) .&. ((exists "z" ((pApp "p" [vt "z"]) .&. ((pApp "q" [vt "z"])))))) .|.-                        (((for_all "y" ((.~.) (pApp "q" [vt "y"]))) .&.-                          ((for_all "z" (((.~.) (pApp "p" [vt "z"])) .|. (((.~.) (pApp "q" [vt "z"]))))))))))) ] }-    , TestFormula-      { name = "pnf 144.1"-      , formula = (for_all "x" (pApp "p" [vt "x"] .|. pApp "r" [vt "y"]) .=>.-                   (exists "y" (exists "z" (pApp "q" [vt "y"] .|. ((.~.) (exists "z" (pApp "p" [vt "z"] .&. pApp "q" [vt "z"])))))))-      , expected = [ PrenexNormalForm -                     (exists "x" -                      (for_all "z"-                       ((((.~.) (pApp "p" [vt "x"])) .&. (((.~.) (pApp "r" [vt "y"])))) .|.-                        (((pApp "q" [vt "x"]) .|. ((((.~.) (pApp "p" [vt "z"])) .|. (((.~.) (pApp "q" [vt "z"])))))))))) ] }-    , let (x, y, u, v) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm)-          fv = fApp (toSkolem "v") [u,x]-          fy = fApp (toSkolem "y") [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) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm) 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 "y") []) .|. (((.~.) (p z)) .|. ((.~.) (q z))))) ] }-    ]--animalKB :: (String, [TTestFormula])-animalKB =-    let x = vt "x"-        y = vt "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 "x") []])],[(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])]])]-       -- 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" [vt "y"])) .|.-                                                                           (((.~.) (pApp "Owns" [vt "x",vt "y"])))) .|.-                                                                          ((pApp "AnimalLover" [vt "x"])))))-                    , ClauseNormalForm (toSS [[((.~.) (pApp "Dog" [vt "y"])),((.~.) (pApp "Owns" [vt "x",vt "y"])),(pApp "AnimalLover" [vt "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" [vt "x"])),((.~.) (pApp "Animal" [vt "y"])),((.~.) (pApp "Kills" [vt "x",vt "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" [vt "x"])),(pApp "Animal" [vt "x"])]])]-       -- animal(X0) | ~cat(X0)-       }-     ])--animalConjectures :: [TTestFormula]-animalConjectures =-    let kills = pApp "Kills"-        jack = fApp "Jack" []-        tuna = fApp "Tuna" []-        curiosity = fApp "Curiosity" [] in--    map (withKB animalKB) $-     [ TestFormula-       { formula = kills [jack, tuna]             -- False-       , name = "jack kills tuna"-       , expected =-           [ FirstOrderFormula ((.~.) (((exists "x" ((pApp "Dog" [vt ("x")]) .&. ((pApp "Owns" [fApp ("Jack") [],vt ("x")])))) .&.-                                        (((for_all "x" ((exists "y" ((pApp "Dog" [vt ("y")]) .&. ((pApp "Owns" [vt ("x"),vt ("y")])))) .=>.-                                                          ((pApp "AnimalLover" [vt ("x")])))) .&.-                                          (((for_all "x" ((pApp "AnimalLover" [vt ("x")]) .=>.-                                                            ((for_all "y" ((pApp "Animal" [vt ("y")]) .=>.-                                                                             (((.~.) (pApp "Kills" [vt ("x"),vt ("y")])))))))) .&.-                                            ((((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]) .|. ((pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.-                                              (((pApp "Cat" [fApp ("Tuna") []]) .&.-                                                ((for_all "x" ((pApp "Cat" [vt ("x")]) .=>.-                                                                 ((pApp "Animal" [vt ("x")])))))))))))))) .=>.-                                       ((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]))))--           , PrenexNormalForm-             (for_all "x"-              (for_all "y"-               (exists "x2"-                ((((pApp ("Dog") [vt ("x2")]) .&.-                   ((pApp ("Owns") [fApp ("Jack") [],vt ("x2")]))) .&.-                  ((((((.~.) (pApp ("Dog") [vt ("y")])) .|.-                      (((.~.) (pApp ("Owns") [vt ("x"),vt ("y")])))) .|.-                     ((pApp ("AnimalLover") [vt ("x")]))) .&.-                    (((((.~.) (pApp ("AnimalLover") [vt ("x")])) .|.-                       ((((.~.) (pApp ("Animal") [vt ("y")])) .|.-                         (((.~.) (pApp ("Kills") [vt ("x"),vt ("y")])))))) .&.-                      ((((pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]) .|.-                         ((pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.-                        (((pApp ("Cat") [fApp ("Tuna") []]) .&.-                          ((((.~.) (pApp ("Cat") [vt ("x")])) .|.-                            ((pApp ("Animal") [vt ("x")]))))))))))))) .&.-                 (((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])))))))-           , ClauseNormalForm-             (toSS-              [[(pApp ("Animal") [vt ("x")]),-                ((.~.) (pApp ("Cat") [vt ("x")]))],-               [(pApp ("AnimalLover") [vt ("x")]),-                ((.~.) (pApp ("Dog") [vt ("y")])),-                ((.~.) (pApp ("Owns") [vt ("x"),vt ("y")]))],-               [(pApp ("Cat") [fApp ("Tuna") []])],-               [(pApp ("Dog") [fApp (toSkolem "x") []])],-               [(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),-                (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])],-               [(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])],-               [((.~.) (pApp ("Animal") [vt ("y")])),-                ((.~.) (pApp ("AnimalLover") [vt ("x")])),-                ((.~.) (pApp ("Kills") [vt ("x"),vt ("y")]))],-               [((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]))]])-           , ChiouKB1-             (Proof-              Invalid-              (S.fromList -               [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])]),-                makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem "x") []])]),-                makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),-                makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]),-                makeINF' ([(pApp ("Animal") [vt ("y")]),(pApp ("AnimalLover") [vt ("x")]),(pApp ("Kills") [vt ("x"),vt ("y")])]) ([]),-                makeINF' ([(pApp ("Cat") [vt ("x")])]) ([(pApp ("Animal") [vt ("x")])]),-                makeINF' ([(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [vt ("x"),vt ("y")])]) ([(pApp ("AnimalLover") [vt ("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 "x") []])],-              [(pApp "Owns" [fApp ("Jack") [],fApp (toSkolem "x") []])],-              [((.~.) (pApp "Dog" [vt ("y")])),-               ((.~.) (pApp "Owns" [vt ("x"),vt ("y")])),-               (pApp "AnimalLover" [vt ("x")])],-              [((.~.) (pApp "AnimalLover" [vt ("x")])),-               ((.~.) (pApp "Animal" [vt ("y")])),-               ((.~.) (pApp "Kills" [vt ("x"),vt ("y")]))],-              [(pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]),-               (pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []])],-              [(pApp "Cat" [fApp ("Tuna") []])],-              [((.~.) (pApp "Cat" [vt ("x")])),-               (pApp "Animal" [vt ("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 = vt "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" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))) .&.-                                                 ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Human" [vt "x"])))))) .=>.-                                                ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))))))-                    , ClauseNormalForm  [[((.~.) (pApp "Human" [vt "x2"])),(pApp "Mortal" [vt "x2"])],-                                          [((.~.) (pApp "Socrates" [vt "x2"])),(pApp "Human" [vt "x2"])],-                                          [(pApp "Socrates" [fApp (toSkolem "x") [vt "x2",vt "x2"]])],-                                          [((.~.) (pApp "Mortal" [fApp (toSkolem "x") [vt "x2",vt "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" [vt "x"]) .=>. ((pApp "Mortal" [vt "x"])))) .&.-                                                 ((for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Human" [vt "x"])))))) .=>.-                                                (((.~.) (for_all' [V "x"] ((pApp "Socrates" [vt "x"]) .=>. ((pApp "Mortal" [vt "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 "x") [x,y]])), (pApp "Human" [fApp (toSkolem "x") [x,y]])],-                                         [(pApp "Socrates" [fApp (toSkolem "x") [x,y]])], [((.~.) (pApp "Mortal" [fApp (toSkolem "x") [x,y]]))]]-                    , ClauseNormalForm [[((.~.) (pApp "Human" [vt "x2"])), (pApp "Mortal" [vt "x2"])],-                                         [((.~.) (pApp "Socrates" [vt "x2"])), (pApp "Human" [vt "x2"])],-                                         [((.~.) (pApp "Socrates" [vt "x"])), (pApp "Mortal" [vt "x"])]] ]-       }-     ]--}--chang43KB :: (String, [TTestFormula])-chang43KB = -    let e = fApp "e" []-        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm) 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 :: TTestFormula-chang43Conjecture =-    let e = (fApp "e" [])-        (x, u, v, w) = (vt "x" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm) 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" [vt ("x"),vt ("y"),vt ("z")]))) .&. ((((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [vt ("x"),vt ("y"),vt ("u")]) .&. ((pApp "P" [vt ("y"),vt ("z"),vt ("v")]))) .&. ((pApp "P" [vt ("u"),vt ("z"),vt ("w")]))) .=>. ((pApp "P" [vt ("x"),vt ("v"),vt ("w")])))) .&. ((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [vt ("x"),vt ("y"),vt ("u")]) .&. ((pApp "P" [vt ("y"),vt ("z"),vt ("v")]))) .&. ((pApp "P" [vt ("x"),vt ("v"),vt ("w")]))) .=>. ((pApp "P" [vt ("u"),vt ("z"),vt ("w")])))))) .&. ((((for_all "x" (pApp "P" [vt ("x"),fApp ("e") [],vt ("x")])) .&. ((for_all "x" (pApp "P" [fApp ("e") [],vt ("x"),vt ("x")])))) .&. (((for_all "x" (pApp "P" [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])) .&. ((for_all "x" (pApp "P" [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])))))))))) .=>. ((for_all "x" ((pApp "P" [vt ("x"),vt ("x"),fApp ("e") []]) .=>. ((for_all' ["u","v","w"] ((pApp "P" [vt ("u"),vt ("v"),vt ("w")]) .=>. ((pApp "P" [vt ("v"),vt ("u"),vt ("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") [vt ("x"),vt ("y"),vt ("z")])))) .&.-                        ((((for_all "x"-                            (for_all "y"-                             (for_all "z"-                              (for_all "u"-                               (for_all "v"-                                (for_all "w"-                                 (((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                                    (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                                   (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.-                                  ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))))))))) .&.-                           ((for_all "x"-                             (for_all "y"-                              (for_all "z"-                               (for_all "u"-                                (for_all "v"-                                 (for_all "w"-                                  (((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                                     (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                                    (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.-                                   ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))))))))) .&.-                          ((((for_all "x" (pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])) .&.-                             ((for_all "x" (pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])))) .&.-                            (((for_all "x" (pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])) .&.-                              ((for_all "x" (pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])))))))))) .&.-                       ((exists "x"-                         ((pApp ("P") [vt ("x"),vt ("x"),fApp ("e") []]) .&.-                          ((exists "u"-                            (exists "v"-                             (exists "w"-                              ((pApp ("P") [vt ("u"),vt ("v"),vt ("w")]) .&.-                               (((.~.) (pApp ("P") [vt ("v"),vt ("u"),vt ("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") [vt ("x"),vt ("y"),vt ("z2")]) .&.-                                   ((((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                                         (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                                        (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.-                                       ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))) .&.-                                      ((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                                          (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                                         (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.-                                        ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))) .&.-                                     ((((pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")]) .&.-                                        ((pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")]))) .&.-                                       (((pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []]) .&.-                                         ((pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []]))))))))) .&.-                                  (((pApp ("P") [vt ("x2"),vt ("x2"),fApp ("e") []]) .&.-                                    (((pApp ("P") [vt ("u2"),vt ("v2"),vt ("w2")]) .&.-                                      (((.~.) (pApp ("P") [vt ("v2"),vt ("u2"),vt ("w2")])))))))))))))))))))-                    , SkolemNormalForm-                      (((pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]]) .&.-                        ((((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                              (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                             (((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])))) .|.-                            ((pApp ("P") [vt ("x"),vt ("v"),vt ("w")]))) .&.-                           ((((((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])) .|.-                               (((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])))) .|.-                              (((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])))) .|.-                             ((pApp ("P") [vt ("u"),vt ("z"),vt ("w")]))))) .&.-                          ((((pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")]) .&.-                             ((pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")]))) .&.-                            (((pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []]) .&.-                              ((pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []]))))))))) .&.-                       (((pApp ("P") [fApp (toSkolem "x") [],fApp (toSkolem "x") [],fApp ("e") []]) .&.-                         (((pApp ("P") [fApp (toSkolem "u") [],fApp (toSkolem "v") [],fApp (toSkolem "w") []]) .&.-                           (((.~.) (pApp ("P") [fApp (toSkolem "v") [],fApp (toSkolem "u") [],fApp (toSkolem "w") []]))))))))-                    , SkolemNumbers (S.fromList [toSkolem "u",toSkolem "v",toSkolem "w",toSkolem "x",toSkolem "z"])-                    -- From our algorithm--                    , ClauseNormalForm-                      (toSS -                      [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]])],-                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),-                        ((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])),-                        ((.~.) (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])),-                        (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])],-                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),-                        ((.~.) (pApp ("P") [vt ("y"),vt ("z"),vt ("v")])),-                        ((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])),-                        (pApp ("P") [vt ("u"),vt ("z"),vt ("w")])],-                       [(pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])],-                       [(pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])],-                       [(pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])],-                       [(pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])],-                       [(pApp ("P") [fApp (toSkolem "x") [],fApp (toSkolem "x") [],fApp ("e") []])],-                       [(pApp ("P") [fApp (toSkolem "u") [],fApp (toSkolem "v") [],fApp (toSkolem "w") []])],-                       [((.~.) (pApp ("P") [fApp (toSkolem "v") [],fApp (toSkolem "u") [],fApp (toSkolem "w") []]))]])--                    -- From the book-{--                    , let (a, b, c) = -                              (fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")],-                               fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")],-                               fApp (toSkolem "x") [vt ("x"),vt ("y"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u"),vt ("v"),vt ("w"),vt ("x2"),vt ("y2"),vt ("z2"),vt ("u2"),vt ("v2"),vt ("w2"),vt ("x3"),vt ("x3"),vt ("x3"),vt ("x3")]) in-                      ClauseNormalForm-                      [[(pApp "P" [vt "x",vt "y",fApp (toSkolem "x") [vt "x",vt "y"]])],-                       [((.~.) (pApp "P" [vt "x",vt "y",vt "u"])),-                        ((.~.) (pApp "P" [vt "y",vt "z",vt "v"])),-                        ((.~.) (pApp "P" [vt "u",vt "z",vt "w"])),-                        (pApp "P" [vt "x",vt "v",vt "w"])],-                       [((.~.) (pApp "P" [vt "x",vt "y",vt "u"])),-                        ((.~.) (pApp "P" [vt "y",vt "z",vt "v"])),-                        ((.~.) (pApp "P" [vt "x",vt "v",vt "w"])),-                        (pApp "P" [vt "u",vt "z",vt "w"])],-                       [(pApp "P" [vt "x",fApp "e" [],vt "x"])],-                       [(pApp "P" [fApp "e" [],vt "x",vt "x"])],-                       [(pApp "P" [vt "x",fApp "i" [vt "x"],fApp "e" []])],-                       [(pApp "P" [fApp "i" [vt "x"],vt "x",fApp "e" []])],-                       [(pApp "P" [vt "x",-                                   vt "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 :: TTestFormula-chang43ConjectureRenamed =-    let e = fApp "e" []-        (x, y, z, u, v, w) = (vt "x" :: TTerm, vt "y" :: TTerm, vt "z" :: TTerm, vt "u" :: TTerm, vt "v" :: TTerm, vt "w" :: TTerm)-        (u2, v2, w2, x2, y2, z2, u3, v3, w3, x3, y3, z3, x4, x5, x6, x7, x8) =-            (vt "u2" :: TTerm, vt "v2" :: TTerm, vt "w2" :: TTerm, vt "x2" :: TTerm, vt "y2" :: TTerm, vt "z2" :: TTerm, vt "u3" :: TTerm, vt "v3" :: TTerm, vt "w3" :: TTerm, vt "x3" :: TTerm, vt "y3" :: TTerm, vt "z3" :: TTerm, vt "x4" :: TTerm, vt "x5" :: TTerm, vt "x6" :: TTerm, vt "x7" :: TTerm, vt "x8" :: TTerm) 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" [vt "x",vt "y",vt "z"]))) .&.-                                    ((for_all' ["x2","y2","z2","u","v","w"] ((((pApp "P" [vt "x2",vt "y2",vt "u"]) .&.-                                                                                          ((pApp "P" [vt "y2",vt "z2",vt "v"]))) .&.-                                                                                         ((pApp "P" [vt "u",vt "z2",vt "w"]))) .=>.-                                                                                        ((pApp "P" [vt "x2",vt "v",vt "w"])))))) .&.-                                   ((for_all' ["x3","y3","z3","u2","v2","w2"] ((((pApp "P" [vt "x3",vt "y3",vt "u2"]) .&.-                                                                                            ((pApp "P" [vt "y3",vt "z3",vt "v2"]))) .&.-                                                                                           ((pApp "P" [vt "x3",vt "v2",vt "w2"]))) .=>.-                                                                                          ((pApp "P" [vt "u2",vt "z3",vt "w2"])))))) .&.-                                  ((for_all "x4" (pApp "P" [vt "x4",fApp "e" [],vt "x4"])))) .&.-                                 ((for_all "x5" (pApp "P" [fApp "e" [],vt "x5",vt "x5"])))) .&.-                                ((for_all "x6" (pApp "P" [vt "x6",fApp "i" [vt "x6"],fApp "e" []])))) .&.-                               ((for_all "x7" (pApp "P" [fApp "i" [vt "x7"],vt "x7",fApp "e" []])))) .=>.-                              ((for_all "x8" ((pApp "P" [vt "x8",vt "x8",fApp "e" []]) .=>.-                                                  ((for_all' ["u3","v3","w3"] ((pApp "P" [vt "u3",vt "v3",vt "w3"]) .=>.-                                                                                    ((pApp "P" [vt "v3",vt "u3",vt "w3"]))))))))))-                    , let a = fApp (toSkolem "u3") []-                          b = fApp (toSkolem "v3") []-                          c = fApp (toSkolem "w3") [] in-                      ClauseNormalForm-                      (toSS-                      [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z") [vt ("x"),vt ("y")]])],-                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),-                        ((.~.) (pApp ("P") [vt ("y"),vt ("z2"),vt ("v")])),-                        ((.~.) (pApp ("P") [vt ("u"),vt ("z2"),vt ("w")])),-                        (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])],-                       [((.~.) (pApp ("P") [vt ("x"),vt ("y"),vt ("u")])),-                        ((.~.) (pApp ("P") [vt ("y"),vt ("z2"),vt ("v")])),-                        ((.~.) (pApp ("P") [vt ("x"),vt ("v"),vt ("w")])),-                        (pApp ("P") [vt ("u"),vt ("z2"),vt ("w")])],-                       [(pApp ("P") [vt ("x"),fApp ("e") [],vt ("x")])],-                       [(pApp ("P") [fApp ("e") [],vt ("x"),vt ("x")])],-                       [(pApp ("P") [vt ("x"),fApp ("i") [vt ("x")],fApp ("e") []])],-                       [(pApp ("P") [fApp ("i") [vt ("x")],vt ("x"),fApp ("e") []])],-                       [(pApp ("P") [fApp (toSkolem "x8") [],fApp (toSkolem "x8") [],fApp ("e") []])],-                       [(pApp ("P") [a,b,c])],-                       [((.~.) (pApp ("P") [b,a,c]))]])                      -                    ]-                }--withKB :: forall formula atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V, FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f) =>-          (String, [TestFormula formula atom v]) -> TestFormula formula atom v -> TestFormula formula atom v-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 atom term v p f. (formula ~ TFormula, atom ~ TAtom, v ~ V,-                                                FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f) =>-               (String, [TestFormula formula atom v]) -> (String, [formula])-kbKnowledge kb = (fst (kb :: (String, [TestFormula formula atom v])), map formula (snd kb))--proofs :: forall term v f. (Term term v f, IsString v, Ord v) => [TestProof TFormula term v]-proofs =-    let -- dog = pApp "Dog" :: [term] -> formula-        -- cat = pApp "Cat" :: [term] -> formula-        -- owns = pApp "Owns" :: [term] -> formula-        kills = pApp "Kills"-        -- animal = pApp "Animal" :: [term] -> formula-        -- animalLover = pApp "AnimalLover" :: [term] -> formula-        socrates = pApp "Socrates"-        -- human = pApp "Human" :: [term] -> formula-        mortal = pApp "Mortal"--        jack = fApp "Jack" []-        tuna = fApp "Tuna" []-        curiosity = fApp "Curiosity" [] in--    [ TestProof-      { proofName = "prove jack kills tuna"-      , proofKnowledge = kbKnowledge animalKB-      , conjecture = kills [jack, tuna]-      , proofExpected = -          [ ChiouKB (S.fromList-                     [WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Dog" [fApp (toSkolem "x") []])]), wiIdent = 1},-                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])]), wiIdent = 1},-                      WithId {wiItem = INF (S.fromList [(pApp "Dog" [vt "y"]),(pApp "Owns" [vt "x",vt "y"])]) (S.fromList [(pApp "AnimalLover" [vt "x"])]), wiIdent = 2},-                      WithId {wiItem = INF (S.fromList [(pApp "Animal" [vt "y"]),(pApp "AnimalLover" [vt "x"]),(pApp "Kills" [vt "x",vt "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" [vt "x"])]) (S.fromList [(pApp "Animal" [vt "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" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),-                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []]),(pApp "Cat" [fApp "Tuna" []])] [],fromList []),-                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList []),-                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),-                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),-                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList []),-                           (inf' [(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],fromList []),-                           (inf' [(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x") []])] [],fromList [])]))-          ]-      }-    , TestProof-      { proofName = "prove curiosity kills tuna"-      , proofKnowledge = kbKnowledge animalKB-      , conjecture = kills [curiosity, tuna]-      , proofExpected =-          [ ChiouKB (S.fromList-                     [WithId {wiItem = inf' []                                 [(pApp "Dog" [fApp (toSkolem "x") []])],                 wiIdent = 1},-                      WithId {wiItem = inf' []                                 [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x") []])], wiIdent = 1},-                      WithId {wiItem = inf' [(pApp "Dog" [vt "y"]),-                                             (pApp "Owns" [vt "x",vt "y"])]  [(pApp "AnimalLover" [vt "x"])],                      wiIdent = 2},-                      WithId {wiItem = inf' [(pApp "Animal" [vt "y"]),-                                             (pApp "AnimalLover" [vt "x"]),-                                             (pApp "Kills" [vt "x",vt "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" [vt "x"])]           [(pApp "Animal" [vt "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") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x") []])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]) ([]),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") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x") []])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x") []])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),-                          (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])-          ]-      }-{--  -- Seems not to terminate-    , let (x, u, v, w, e) = (vt "x", vt "u", vt "v", vt "w", vt "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 = vt "x" in-      TestProof-      { proofName = "socrates is mortal"-      , proofKnowledge = kbKnowledge (socratesKB)-      , conjecture = for_all "x" (socrates [x] .=>. mortal [x])-      , proofExpected = -         [ ChiouKB (S.fromList-                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},-                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])-         , ChiouResult (True,-                        S.fromList -                        [(makeINF' ([]) ([]),fromList []),-                         (makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x") []])]),fromList []),-                         (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x") []])]),fromList []),-                         (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x") []])]),fromList []),-                         (makeINF' ([(pApp ("Mortal") [fApp (toSkolem "x") []])]) ([]),fromList [])])]-      }-    , let x = vt "x" in-      TestProof-      { proofName = "socrates is not mortal"-      , proofKnowledge = kbKnowledge (socratesKB)-      , conjecture = (.~.) (for_all "x" (socrates [x] .=>. mortal [x]))-      , proofExpected = -         [ ChiouKB (S.fromList-                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},-                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])-         , ChiouResult (False-                       ,(S.fromList [(inf' [(pApp "Socrates" [vt "x"])] [(pApp "Mortal" [vt "x"])],fromList [("x",vt "x")])]))]-      }-    , let x = vt "x" in-      TestProof-      { proofName = "socrates exists and is not mortal"-      , proofKnowledge = kbKnowledge (socratesKB)-      , conjecture = (.~.) (exists "x" (socrates [x]) .&. for_all "x" (socrates [x] .=>. mortal [x]))-      , proofExpected = -         [ ChiouKB (S.fromList-                    [WithId {wiItem = inf' [(pApp "Human" [vt "x"])] [(pApp "Mortal" [vt "x"])], wiIdent = 1},-                     WithId {wiItem = inf' [(pApp "Socrates" [vt "x"])] [(pApp "Human" [vt "x"])], wiIdent = 2}])-         , ChiouResult (False,-                        S.fromList [(makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x") []])]),fromList []),-                                    (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x") []])]),fromList []),-                                    (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x") []])]),fromList []),-                                    (makeINF' ([(pApp ("Socrates") [vt ("x")])]) ([(pApp ("Mortal") [vt ("x")])]),fromList [("x",vt ("x"))])])-         ]-      }-    ]--inf' = makeINF'--toLL = map S.toList . S.toList-toSS = S.fromList . map S.fromList
− Data/Logic/Tests/HUnit.hs 
@@ -1,67 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, RankNTypes #-}-module Data.Logic.Tests.HUnit-    ( Test(..)-    , Assertion-    , T.assertEqual-    , convert-    , TestFormula-    , TestFormulaEq-    ) where--import Data.Logic.Classes.Apply (Apply)-import Data.Logic.Classes.Equals (AtomEq)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula)-import Data.Logic.Classes.Term (Term)-import Data.Logic.Types.Harrison.FOL (Function(..))-import Data.String (IsString(fromString))-import qualified Test.HUnit as T--type Assertion t = IO ()---- | HUnit Test type with an added phantom type parameter.  To run--- such a test you use the convert function below:--- @---   :load Data.Logic.Tests.Harrison.Meson---   :m +Data.Logic.Tests.HUnit---   :m +Test.HUnit---   runTestTT (convert tests)--- @-data Test t-  = TestCase (Assertion t)-  | TestList [Test t]-  | TestLabel String (Test t)-  | Test0 T.Test--convert :: Test t -> T.Test-convert (TestCase assertion) = T.TestCase assertion-convert (TestList tests) = T.TestList (map convert tests)-convert (TestLabel label test) = T.TestLabel label (convert test)-convert (Test0 test) = test--class (FirstOrderFormula formula atom v,-       Apply atom p term,-       Term term v f,-       Eq formula, Ord formula, Show formula,-       Eq p,-       IsString v, IsString p, IsString f, Ord f, Ord p,-       Eq term, Show term, Ord term,-       Show v) => TestFormula formula atom term v p f--class (FirstOrderFormula formula atom v,-       AtomEq atom p term,-       Term term v f,-       Eq formula, Ord formula, Show formula,-       Eq p,-       IsString v, IsString p, IsString f, Ord f, Ord p,-       Eq term, Show term, Ord term,-       Show v) => TestFormulaEq formula atom term v p f--{--type Test' = forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-type Formula' = forall formula atom term v p f. TestFormula formula atom term v p f => formula-type TestEq' = forall formula atom term v p f. TestFormulaEq formula atom term v p f => Test formula-type FormulaEq' = forall formula atom term v p f. TestFormulaEq formula atom term v p f => formula--}--instance IsString Function where-    fromString = FName
− Data/Logic/Tests/Harrison/Common.hs 
@@ -1,10 +0,0 @@-{-# LANGUAGE FlexibleInstances, StandaloneDeriving #-}-module Data.Logic.Tests.Harrison.Common where--import Data.Logic.Types.Harrison.Equal (FOLEQ(..))-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))--deriving instance Show FOLEQ-deriving instance Show (Formula FOLEQ)--
− Data/Logic/Tests/Harrison/Equal.hs 
@@ -1,256 +0,0 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}-{-# OPTIONS_GHC -Wall #-}-module Data.Logic.Tests.Harrison.Equal where---- ========================================================================= --- First order logic with equality.                                          ---                                                                           --- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)  --- ========================================================================= --import Control.Applicative.Error (Failing(..))-import Data.Logic.Classes.Combine (Combinable(..), (∧), (⇒))---import Data.Logic.Classes.Constants (true)-import Data.Logic.Classes.Equals ((.=.), pApp)-import Data.Logic.Classes.FirstOrder ((∃), (∀))---import Data.Logic.Classes.Pretty (Pretty(pretty))-import Data.Logic.Classes.Skolem (Skolem(..))-import Data.Logic.Classes.Term (Term(..))-import Data.Logic.Harrison.Equal (equalitize, function_congruence)-import Data.Logic.Harrison.Meson (meson)-import Data.Logic.Harrison.Skolem (runSkolem)-import Data.Logic.Tests.Common (render)-import Data.Logic.Types.Harrison.FOL (TermType(..))-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))-import Data.Logic.Types.Harrison.Equal (FOLEQ(..), PredName)-import qualified Data.Map as Map-import qualified Data.Set as Set-import Data.String (IsString(fromString))-import Data.Logic.Tests.HUnit---- type TF = TestFormula (Formula FOL) FOL TermType String String Function--- type TFE = TestFormulaEq (Formula FOLEQ) FOLEQ TermType String String Function--tests :: Test (Formula FOLEQ)-tests = TestLabel "Data.Logic.Tests.Harrison.Equal" $ TestList [test01, test02, test03, test04]---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test01 :: Test (Formula FOLEQ)-test01 = TestCase $ assertEqual "function_congruence" expected input-    where input = map function_congruence [(fromString "f", 3 :: Int), (fromString "+",2)]-          expected :: [Set.Set (Formula FOLEQ)]-          expected = [Set.fromList-                      [(∀) x1-                       ((∀) x2-                        ((∀) x3-                         ((∀) y1-                          ((∀) y2-                           ((∀) y3 ((((vt x1) .=. (vt y1)) ∧ (((vt x2) .=. (vt y2)) ∧ ((vt x3) .=. (vt y3)))) ⇒-                                          ((fApp (fromString "f") [vt x1,vt x2,vt x3]) .=. (fApp (fromString "f") [vt y1,vt y2,vt y3]))))))))],-                      Set.fromList-                      [(∀) x1-                       ((∀) x2-                        ((∀) y1-                         ((∀) y2 ((((vt x1) .=. (vt y1)) ∧ ((vt x2) .=. (vt y2))) ⇒-                                        ((fApp (fromString "+") [vt x1,vt x2]) .=. (fApp (fromString "+") [vt y1,vt y2]))))))]]-          x1 = fromString "x1"-          x2 = fromString "x2"-          x3 = fromString "x3"-          y1 = fromString "y1"-          y2 = fromString "y2"-          y3 = fromString "y3"---- ------------------------------------------------------------------------- --- A simple example (see EWD1266a and the application to Morley's theorem).  --- ------------------------------------------------------------------------- --test :: (Show a, Eq a) => String -> a -> a -> Test (Formula FOLEQ)-test label expected input = TestLabel label $ TestCase $ assertEqual label expected input--test02 :: Test (Formula FOLEQ)-test02 = test "equalitize 1 (p. 241)" (expected, expectedProof) input-    where input = (render ewd, runSkolem (meson (Just 10) ewd))-          ewd = equalitize fm :: Formula FOLEQ-          fm :: Formula FOLEQ-          fm = ((∀) "x" (fx ⇒ gx)) ∧-               ((∃) "x" fx) ∧-               ((∀) "x" ((∀) "y" (gx ∧ gy ⇒ x .=. y))) ⇒-               ((∀) "y" (gy ⇒ fy))-          fx = pApp' "f" [x]-          gx = pApp' "g" [x]-          fy = pApp' "f" [y]-          gy = pApp' "g" [y]-          x = vt "x"-          y = vt "y"-          z = vt "z"-          x1 = vt "x1"-          y1 = vt "y1"-          fx1 = pApp' "f" [x1]-          gx1 = pApp' "g" [x1]-          fy1 = pApp' "f" [y1]-          gy1 = pApp' "g" [y1]-          -- y1 = fromString "y1"-          -- z = fromString "z"-          expected = render $-              ((∀) "x" (x .=. x)) .&.-              ((∀) "x" ((∀) "y" ((∀) "z" (x .=. y .&. x .=. z .=>. y .=. z)))) .&.-              ((∀) "x1" ((∀) "y1" (x1 .=. y1 .=>. fx1 .=>. fy1))) .&.-              ((∀) "x1" ((∀) "y1" (x1 .=. y1 .=>. gx1 .=>. gy1))) .=>.-              ((∀) "x" (fx .=>. gx)) .&.-              ((∃) "x" (fx)) .&.-              ((∀) "x" ((∀) "y" (gx .&. gy .=>. x .=. y))) .=>.-              ((∀) "y" (gy .=>. fy))-{--          -- I don't yet know if this is right.  Almost certainly not.-          expectedProof = Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2),1),-                                        Success ((Map.fromList [("_0",vt "_2"),("_1",vt "_2")],0,3),1),-                                        Success ((Map.fromList [("_0",fApp (Skolem 1) [] :: TermType)],0,1),1),-                                        Success ((Map.fromList [("_0",fApp (Skolem 2) [] :: TermType)],0,1),1)]--          expected = ("<<(forall x. x = x) /\ " ++-                      "    (forall x y z. x = y /\ x = z ==> y = z) /\ " ++-                      "    (forall x1 y1. x1 = y1 ==> f(x1) ==> f(y1)) /\ " ++-                      "    (forall x1 y1. x1 = y1 ==> g(x1) ==> g(y1)) ==> " ++-                      "    (forall x. f(x) ==> g(x)) /\ " ++-                      "    (exists x. f(x)) /\ (forall x y. g(x) /\ g(y) ==> x = y) ==> " ++-                      "    (forall y. g(y) ==> f(y))>> ")--}-          expectedProof =-              Set.fromList [Success ((Map.fromList [(fromString "_0",vt "_2"),-                                                    (fromString "_1",fApp (toSkolem "y") []),-                                                    (fromString "_2",vt "_4"),-                                                    (fromString "_3",fApp (toSkolem "y") []),-                                                    (fromString "_4",fApp (toSkolem "x") [])],0,5),6)]-{--          expectedProof =-              Set.singleton (Success ((Map.fromList [(fromString "_0",vt' "_2"),-                                                     (fromString "_1",fApp (toSkolem "x") []),-                                                     (fromString "_2",vt' "_4"),-                                                     (fromString "_3",fApp (toSkolem "x") []),-                                                     (fromString "_4",fApp (toSkolem "x") []),-                                                     (fromString "_5",fApp (toSkolem "x") [])], 0, 6), 5))-          fApp' :: String -> [term] -> term-          fApp' s ts = fApp (fromString s) ts-          for_all' s = for_all (fromString s)-          exists' s = exists (fromString s)--}-          pApp' :: String -> [TermType] -> Formula FOLEQ-          pApp' s ts = pApp (fromString s :: PredName) ts-          --vt' :: String -> TermType-          --vt' s = vt (fromString s)---- ------------------------------------------------------------------------- --- Wishnu Prasetya's example (even nicer with an "exists unique" primitive). --- ------------------------------------------------------------------------- --wishnu :: Formula FOLEQ-wishnu = ((∃) ("x") ((x .=. f[g[x]]) ∧ (∀) ("x'") ((x' .=. f[g[x']]) ⇒ (x .=. x')))) .<=>.-         ((∃) ("y") ((y .=. g[f[y]]) ∧ (∀) ("y'") ((y' .=. g[f[y']]) ⇒ (y .=. y'))))-    where-      x = vt "x"-      y = vt "y"-      x' = vt "x'"-      y' = vt "y"-      f terms = fApp (fromString "f") terms-      g terms = fApp (fromString "g") terms--test03 :: Test (Formula FOLEQ)-test03 = TestLabel "equalitize 2" $ TestCase $ assertEqual "equalitize 2 (p. 241)" (render expected, expectedProof) input-    where -- This depth is not sufficient to finish. It shoudl work with 16, but that takes a long time.-          input = (render (equalitize wishnu), runSkolem (meson (Just 50) wishnu))-          x = vt "x" :: TermType-          x1 = vt "x1"-          y = vt "y"-          y1 = vt "y1"-          z = vt "z"-          x' = vt "x'"-          y' = vt "y"-          f terms = fApp (fromString "f") terms-          g terms = fApp (fromString "g") terms-          expected :: Formula FOLEQ-          expected =-                     ((∀) "x" (x .=. x)) .&.-                     ((∀) "x" . (∀) "y" . (∀) "z" $ (x .=. y .&. x .=. z .=>. y .=. z)) .&.-                     ((∀) "x1" . (∀) "y1" $ (x1 .=. y1 .=>. f[x1] .=. f[y1])) .&.-                     ((∀) "x1" . (∀) "y1" $ (x1 .=. y1 .=>. g[x1] .=. g[y1])) .=>.-                     (((∃) "x" $ x .=. f[g[x]] .&. ((∀) "x'" $ (x' .=. f[g[x']] .=>. x .=. x'))) .<=>.-                      ((∃) "y" $ y .=. g[f[y]] .&. ((∀) "y'" $ (y' .=. g[f[y']] .=>. y .=. y'))))-          expectedProof =-              Set.fromList [Failure ["Exceeded maximum depth limit"]]-{--              Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2 :: Map.Map String TermType),1),-                            Success ((Map.fromList [("_0",vt "_1"),("_1",fApp "f" [fApp "g" [vt "_0"]])],0,2),1),-                            Success ((Map.fromList [("_0",vt "_1"),("_1",fApp "g" [fApp "f" [vt "_0"]])],0,2),1),-                            Success ((Map.fromList [("_0",vt "_1"),("_2",fApp (fromSkolem 2) [vt "_0"])],0,3),1),-                            Success ((Map.fromList [("_0",vt "_2"),("_1",vt "_2")],0,3),1)] -}---- ------------------------------------------------------------------------- --- More challenging equational problems. (Size 18, 61814 seconds.)           --- ------------------------------------------------------------------------- --test04 :: Test (Formula FOLEQ)-test04 = test "equalitize 3 (p. 248)" (render expected, expectedProof) input-    where-      input = (render (equalitize fm), runSkolem (meson (Just 20) . equalitize $ fm))-      fm :: Formula FOLEQ-      fm = ((∀) "x" . (∀) "y" . (∀) "z") ((*) [x', (*) [y', z']] .=. (*) [((*) [x', y']), z']) ∧-           (∀) "x" ((*) [one, x'] .=. x') ∧-           (∀) "x" ((*) [i [x'], x'] .=. one) ⇒-           (∀) "x" ((*) [x', i [x']] .=. one)-      x' = vt "x" :: TermType-      y' = vt "y" :: TermType-      z' = vt "z" :: TermType-      (*) = fApp (fromString "*")-      i = fApp (fromString "i")-      one = fApp (fromString "1") []-      expected :: Formula FOLEQ-      expected =-          ((∀) "x" ((vt "x") .=. (vt "x")) .&.-           ((∀) "x" ((∀) "y" ((∀) "z" ((((vt "x") .=. (vt "y")) .&. ((vt "x") .=. (vt "z"))) .=>. ((vt "y") .=. (vt "z"))))) .&.-            ((∀) "x1" ((∀) "x2" ((∀) "y1" ((∀) "y2" ((((vt "x1") .=. (vt "y1")) .&. ((vt "x2") .=. (vt "y2"))) .=>.-                                                                     ((fApp "*" [vt "x1",vt "x2"]) .=. (fApp "*" [vt "y1",vt "y2"])))))) .&.-             (∀) "x1" ((∀) "y1" (((vt "x1") .=. (vt "y1")) .=>. ((fApp "i" [vt "x1"]) .=. (fApp "i" [vt "y1"]))))))) .=>.-          ((((∀) "x" ((∀) "y" ((∀) "z" ((fApp "*" [vt "x",fApp "*" [vt "y",vt "z"]]) .=. (fApp "*" [fApp "*" [vt "x",vt "y"],vt "z"])))) .&.-             (∀) "x" ((fApp "*" [fApp "1" [],vt "x"]) .=. (vt "x"))) .&.-            (∀) "x" ((fApp "*" [fApp "i" [vt "x"],vt "x"]) .=. (fApp "1" []))) .=>.-           (∀) "x" ((fApp "*" [vt "x",fApp "i" [vt "x"]]) .=. (fApp "1" [])))-      expectedProof :: Set.Set (Failing ((Map.Map String TermType, Int, Int), Int))-      expectedProof =-          Set.fromList-                 [Success ((Map.fromList-                                   [( "_0",  (*) [one, vt' "_3"]),-                                    ( "_1",  (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),-                                    ( "_2",  one),-                                    ( "_3",  (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),-                                    ( "_4",  vt' "_8"),-                                    ( "_5",  (*) [one, vt' "_3"]),-                                    ( "_6",  one),-                                    ( "_7",  vt' "_11"),-                                    ( "_8",  vt' "_12"),-                                    ( "_9",  (*) [one, vt' "_3"]),-                                    ("_10", (*) [vt' "_13",(*) [vt' "_14", vt' "_15"]]),-                                    ("_11", (*) [(*) [vt' "_13", vt' "_14"], vt' "_15"]),-                                    ("_12", (*) [vt' "_19", vt' "_18"]),-                                    ("_13", vt' "_16"),-                                    ("_14", vt' "_21"),-                                    ("_15", (*) [vt' "_22", vt' "_23"]),-                                    ("_16", vt' "_20"),-                                    ("_17", (*) [vt' "_14", vt' "_15"]),-                                    ("_18", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"]),-                                    ("_19", vt' "_20"),-                                    ("_20", i [vt' "_28"]),-                                    ("_21", vt' "_28"),-                                    ("_22", fApp (toSkolem "x") []),-                                    ("_23", i [fApp (toSkolem "x") []]),-                                    ("_24", (*) [vt' "_13", vt' "_14"]),-                                    ("_25", (*) [vt' "_22", vt' "_23"]),-                                    ("_26", (*) [fApp (toSkolem "x") [],i [fApp (toSkolem "x") []]]),-                                    ("_27", one),-                                    ("_28", vt' "_30"),-                                    ("_29", (*) [vt' "_22", vt' "_23"]),-                                    ("_30", (*) [(*) [vt' "_21", vt' "_22"], vt' "_23"])],-                            0,31),13)]-      vt' = vt . fromString
− Data/Logic/Tests/Harrison/FOL.hs 
@@ -1,226 +0,0 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes,-             ScopedTypeVariables, TypeFamilies, TypeSynonymInstances #-}-{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}-module Data.Logic.Tests.Harrison.FOL-    ( tests1-    , tests2-    , example1-    , example2-    , example3-    , example4-    ) where--import Control.Applicative ((<$>), (<*>))-import Control.Applicative.Error (Failing(..))-import Control.Monad (filterM)-import Data.Logic.Classes.Apply (pApp)-import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..))-import Data.Logic.Classes.Constants (false)-import Data.Logic.Classes.Equals (AtomEq(..), (.=.))-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))-import qualified Data.Logic.Classes.FirstOrder as C-import Data.Logic.Classes.Negate ((.~.))-import Data.Logic.Classes.Term (Term(vt, fApp, foldTerm))-import Data.Logic.Classes.Variable (Variable(..))-import Data.Logic.Harrison.Lib ((|->))-import Data.Logic.Tests.HUnit-import Data.Logic.Types.Harrison.Equal (FOLEQ, PredName(..))-import Data.Logic.Types.Harrison.FOL (TermType(..), FOL(..), Function(..))-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))-import qualified Data.Map as Map-import qualified Data.Set as Set-import Prelude hiding (pred)--tests1 :: TestFormula formula atom term v p f => Test formula-tests1 = TestLabel "Data.Logic.Tests.Harrison.FOL" $-        TestList [test01, test02, test03, test04, test05,-                  test06, test07, test08, test09]-tests2 :: TestFormulaEq formula atom term v p f => Test formula-tests2 = TestLabel "Data.Logic.Tests.Harrison.FOL" $-         TestList [{-test10, test11, test12-}]---- ------------------------------------------------------------------------- --- Semantics, implemented of course for finite domains only.                 --- ------------------------------------------------------------------------- --termval :: (Term term v f, Show v) =>-           ([a], f -> [a] -> a, p -> [a] -> Bool)-        -> Map.Map v a-        -> term-        -> Failing a-termval m@(_domain, func, _pred) v tm =-    foldTerm (\ x -> maybe (Failure ["Undefined variable: " ++ show x]) Success (Map.lookup x v))-             (\ f args -> mapM (termval m v) args >>= return . func f)-             tm--holds :: forall formula atom term v p f a.-         (FirstOrderFormula formula atom v, AtomEq atom p term, Term term v f, Show v, Eq a) =>-         ([a], f -> [a] -> a, p -> [a] -> Bool)-      -> Map.Map v a-      -> formula-      -> Failing Bool-holds m@(domain, _func, pred) v fm =-    foldFirstOrder qu co tf at fm-    where-      qu op x p = mapM (\ a -> holds m ((|->) x a v) p) domain >>= return . (asPred op) (== True)-      asPred C.Exists = any-      asPred C.Forall = all-      co ((:~:) p) = holds m v p >>= return . not-      co (BinOp p (:|:) q) = (||) <$> (holds m v p) <*> (holds m v q)-      co (BinOp p (:&:) q) = (&&) <$> (holds m v p) <*> (holds m v q)-      co (BinOp p (:=>:) q) = (||) <$> (not <$> (holds m v p)) <*> (holds m v q)-      co (BinOp p (:<=>:) q) = (==) <$> (holds m v p) <*> (holds m v q)-      tf x = Success x-      at :: atom -> Failing Bool-      at = foldAtomEq (\ r args -> mapM (termval m v) args >>= return . pred r) return (\ t1 t2 -> return $ termval m v t1 == termval m v t2)---- | This becomes a method in FirstOrderFormulaEq, so it is not exported here.--- (.=.) :: TermType -> TermType -> Formula FOL--- a .=. b = Atom (R "=" [a, b])---- ---------------------------------------------------------------------------- Example.                                                                 --- ---------------------------------------------------------------------------example1 :: TermType-example1 = fApp "sqrt" [fApp "-" [fApp "1" [], fApp "cos" [fApp "power" [fApp "+" [vt "x", vt "y"], fApp "2" []]]]]--- example1 = Fn "sqrt" [Fn "-" [Fn "1" [], Fn "cos" [Fn "power" [Fn "+" [vt "x", vt "y"], Fn "2" []]]]]---- ---------------------------------------------------------------------------- Trivial example of "x + y < z".                                           --- ------------------------------------------------------------------------- --example2 :: Formula FOL-example2 = pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"]--- example2 = Atom (R "<" [Fn "+" [Var "x", Var "y"], Var "z"])---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --example3 :: Formula FOL-example3 = (for_all "x" (pApp "<" [vt "x", fApp "2" []] .=>.-                         pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false-example4 :: TermType-example4 = fApp "*" [fApp "2" [], vt "x"]---- ------------------------------------------------------------------------- --- Examples of particular interpretations.                                   --- ------------------------------------------------------------------------- --boolInterp :: ([Bool], Function -> [Bool] -> Bool, PredName -> [Bool] -> Bool)-boolInterp =-    ([False, True],func,pred)-    where-      func f args =-          case (f,args) of-            ("0",[]) -> False-            ("1",[]) -> True-            ("+",[x, y]) -> not (x == y)-            ("*",[x, y]) -> x && y-            _ -> error "uninterpreted function"-      pred p args =-          case (p,args) of-            ((:=:), [x, y]) -> x == y-            _ -> error "uninterpreted predicate"--modInterp :: Integer-          -> ([Integer],-              Function -> [Integer] -> Integer,-              PredName -> [Integer] -> Bool)-modInterp n =-    ([0..(n-1)],func,pred)-    where-      func :: Function -> [Integer] -> Integer-      func f args =-          case (f,args) of-            ("0",[]) -> 0-            ("1",[]) -> 1 `mod` n-            ("+",[x, y]) -> (x + y) `mod` n-            ("*",[x, y]) -> (x * y) `mod` n-            _ -> error "uninterpreted function"-      pred :: PredName -> [Integer] -> Bool-      pred p args =-          case (p,args) of-            ((:=:),[x, y]) -> x == y-            _ -> error "uninterpreted predicate"---- test01 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test01 = TestCase $ assertEqual "holds bool test (p. 126)" expected input-    where input = holds boolInterp Map.empty (for_all "x" (vt "x" .=. fApp "0" [] .|. vt "x" .=. fApp "1" []) :: Formula FOLEQ)-          expected = Success True--- test02 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test02 = TestCase $ assertEqual "holds mod test 1 (p. 126)" expected input-    where input =  holds (modInterp 2) Map.empty (for_all "x" (vt "x" .=. (fApp "0" [] :: TermType) .|. vt "x" .=. (fApp "1" [] :: TermType)) :: Formula FOLEQ)-          expected = Success True--- test03 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test03 = TestCase $ assertEqual "holds mod test 2 (p. 126)" expected input-    where input =  holds (modInterp 3) Map.empty (for_all "x" (vt "x" .=. fApp "0" [] .|. vt "x" .=. fApp "1" []) :: Formula FOLEQ)-          expected = Success False---- test04 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test04 = TestCase $ assertEqual "holds mod test 3 (p. 126)" expected input-    where input = filterM (\ n -> holds (modInterp n) Map.empty fm) [1..45]-                  where fm = for_all "x" ((.~.) (vt "x" .=. fApp "0" []) .=>. exists "y" (fApp "*" [vt "x", vt "y"] .=. fApp "1" [])) :: Formula FOLEQ-          expected = Success [1,2,3,5,7,11,13,17,19,23,29,31,37,41,43]---- test05 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test05 = TestCase $ assertEqual "holds mod test 4 (p. 129)" expected input-    where input = holds (modInterp 3) Map.empty ((for_all "x" (vt "x" .=. fApp "0" [])) .=>. fApp "1" [] .=. fApp "0" [] :: Formula FOLEQ)-          expected = Success True--- test06 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test06 = TestCase $ assertEqual "holds mod test 5 (p. 129)" expected input-    where input = holds (modInterp 3) Map.empty (for_all "x" (vt "x" .=. fApp "0" [] .=>. fApp "1" [] .=. fApp "0" []) :: Formula FOLEQ)-          expected = Success False---- ------------------------------------------------------------------------- --- Variant function and examples.                                            --- ------------------------------------------------------------------------- ---- test07 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test07 = TestCase $ assertEqual "variant 1 (p. 133)" expected input-    where input = variant "x" (Set.fromList ["y", "z"]) :: String-          expected = "x"--- test08 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test08 = TestCase $ assertEqual "variant 2 (p. 133)" expected input-    where input = variant "x" (Set.fromList ["x", "y"]) :: String-          expected = "x'"--- test09 :: forall formula atom term v p f. TestFormula formula atom term v p f => Test formula-test09 = TestCase $ assertEqual "variant 3 (p. 133)" expected input-    where input = variant "x" (Set.fromList ["x", "x'"]) :: String-          expected = "x''"---- ------------------------------------------------------------------------- --- Examples.                                                                 --- ------------------------------------------------------------------------- -{---- test10 :: forall formula atom term v p f. TestFormulaEq formula atom term v p f => Test formula-test10 =-    let (x, x', y) = (fromString "x", fromString "x'", fromString "y") in-    TestCase $ assertEqual "subst 1 (p. 134)" expected input-    where input = subst (y |=> vt x) (C.for_all x (vt x .=. vt y))-          expected = C.for_all x' (vt x' .=. vt x)--test11 :: forall formula atom term v p f. TestFormulaEq formula atom term v p f => Test formula-test11 = TestCase $ assertEqual "subst 2 (p. 134)" expected input-    where input = subst ("y" |=> Var "x") (C.for_all "x" (C.for_all "x'" ((vt "x" .=. vt "y") .=>. (vt "x" .=. vt "x'"))))-          expected = H.Forall "x'" (H.Forall "x''" (Imp (Atom (R "=" [Var "x'",Var "x"])) (Atom (R "=" [Var "x'",Var "x''"]))))--test12 :: forall formula atom term v p f. TestFormulaEq formula atom term v p f => Test formula-test12 = TestCase $ assertEqual "show first order formula 1" expected input-    where input = map show fms-          expected = ["((pApp \"p\" []) .&. (pApp \"q\" [])) .|. (pApp \"r\" [])",-                      "(pApp \"p\" []) .&. (pApp \"q\" []) .|. (pApp \"r\" [])",-                      "((pApp \"p\" []) .&. (pApp \"q\" [])) .|. (pApp \"r\" [])",-                      "(pApp \"p\" []) .&. ((.~.)(pApp \"q\" []))",-                      "for_all (fromString (\"x\")) ((pApp \"p\" []) .&. (pApp \"q\" []))"]-          fms :: [formula]-          fms = [(p .&. q .|. r),-                 (p .&. (q .|. r)),-                 ((p .&. q) .|. r),-                 (p .&. ((.~.) q)),-                 (for_all "x" (p .&. q))]-          p = pApp "p" []-          q = pApp "q" []-          r = pApp "r" []--}
− Data/Logic/Tests/Harrison/Main.hs 
@@ -1,40 +0,0 @@-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeSynonymInstances #-}-module Data.Logic.Tests.Harrison.Main (tests) where--import Data.Logic.Classes.Pretty (pretty)-import qualified Data.Logic.Harrison.Lib as Lib-import qualified Data.Logic.Tests.Harrison.Equal as Equal-import qualified Data.Logic.Tests.Harrison.FOL as FOL-import qualified Data.Logic.Tests.Harrison.Meson as Meson-import qualified Data.Logic.Tests.Harrison.Prop as Prop-import qualified Data.Logic.Tests.Harrison.Resolution as Resolution-import qualified Data.Logic.Tests.Harrison.Skolem as Skolem-import qualified Data.Logic.Tests.Harrison.Unif as Unif-import Data.Logic.Types.Harrison.Equal (FOLEQ, PredName)-import Data.Logic.Types.Harrison.FOL (FOL, TermType, Function)-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..))-import Data.Logic.Tests.HUnit-import qualified Test.HUnit as T---import Data.String (IsString)--instance TestFormula (Formula FOL) FOL TermType String String Function-instance TestFormulaEq (Formula FOLEQ) FOLEQ TermType String PredName Function--instance Show (Formula FOL) where-    show = show . pretty--main = T.runTestTT tests--tests :: T.Test-tests =-    T.TestList-         [ Lib.tests-         , Prop.tests-         , convert (FOL.tests1 :: Test (Formula FOL))-         , convert (FOL.tests2 :: Test (Formula FOLEQ))-         , Unif.tests-         , Skolem.tests-         , convert (Resolution.tests :: Test (Formula FOLEQ))-         , convert (Equal.tests :: Test (Formula FOLEQ))-         , convert (Meson.tests :: Test (Formula FOLEQ))-         ]
− Data/Logic/Tests/Harrison/Meson.hs 
@@ -1,123 +0,0 @@-{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}-{-# OPTIONS_GHC -Wall #-}-module Data.Logic.Tests.Harrison.Meson where--import Control.Applicative.Error (Failing(..))-import qualified Data.Map as Map-import qualified Data.Set as Set-import Data.Logic.Classes.Equals (pApp)-import Data.Logic.Classes.Combine ((.&.), (.=>.), (.|.))-import Data.Logic.Classes.Constants (true)-import Data.Logic.Classes.FirstOrder (exists, for_all)-import Data.Logic.Classes.Negate ((.~.))-import Data.Logic.Classes.Skolem (Skolem(..))-import Data.Logic.Classes.Term (Term(vt, fApp))-import Data.Logic.Harrison.FOL (generalize, list_conj)-import Data.Logic.Harrison.Meson(meson)-import Data.Logic.Harrison.Normal (simpdnf)-import Data.Logic.Harrison.Skolem (runSkolem, askolemize)-import Data.Logic.Tests.Common (render)-import Data.Logic.Tests.Harrison.Resolution (dpExampleFm)-import Data.Logic.Tests.HUnit-import Data.Logic.Types.Harrison.Equal (FOLEQ)-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula)-import Data.String (IsString(fromString))-import Prelude hiding (negate)--- import Test.HUnit (Test(TestCase, TestLabel), assertEqual)--tests :: Test (Formula FOLEQ)-tests = TestLabel "Data.Logic.Tests.Harrison.Meson" $-        TestList [test01, test02]---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test01 :: Test (Formula FOLEQ)-test01 = TestLabel "Data.Logic.Tests.Harrison.Meson" $ TestCase $ assertEqual "meson dp example (p. 220)" expected input-    where input = runSkolem (meson (Just 10) (dpExampleFm :: Formula FOLEQ))-          expected = Set.singleton (-                                    -- Success ((Map.empty, 0, 0), 8)-                                    Success ((Map.fromList [(fromString "_0",vt' "_6"),-                                                            (fromString "_1",vt' "_2"),-                                                            (fromString "_10",fApp (toSkolem "z") [vt' "_6",vt' "_7"]),-                                                            (fromString "_11",fApp (toSkolem "z") [vt' "_6",vt' "_7"]),-                                                            (fromString "_12",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_13",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_14",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_15",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),-                                                            (fromString "_16",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),-                                                            (fromString "_17",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),-                                                            (fromString "_3",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_4",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_5",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_7",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_8",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),-                                                            (fromString "_9",fApp (toSkolem "z") [vt' "_6",vt' "_7"])],0,18),8)-                                   )-          vt' = vt . fromString--test02 :: Test (Formula FOLEQ)-test02 =-    TestLabel "Data.Logic.Tests.Harrison.Meson" $-    TestList [TestCase (assertEqual "meson dp example, step 1 (p. 220)"-                                    (render (exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.-                                                                                  (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))))-                                    (render dpExampleFm)),-              TestCase (assertEqual "meson dp example, step 2 (p. 220)"-                                    (render (exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.-                                                                                  (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))))-                                    (render (generalize dpExampleFm))),-              TestCase (assertEqual "meson dp example, step 3 (p. 220)"-                                    (render ((.~.)(exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.-                                                                                        (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))) :: Formula FOLEQ))-                                    (render ((.~.) (generalize dpExampleFm)))),-              TestCase (assertEqual "meson dp example, step 4 (p. 220)"-                                    (render (for_all "x" . for_all "y" $-                                             f[x,y] .&.-                                             ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.-                                             (f[x,y] .&. g[x,y]) .&.-                                             (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))))-                                    (render (runSkolem (askolemize ((.~.) (generalize dpExampleFm))) :: Formula FOLEQ))),-              TestCase (assertEqual "meson dp example, step 5 (p. 220)"-                                    (Set.map (Set.map render)-                                     (Set.fromList-                                      [Set.fromList [for_all "x" . for_all "y" $-                                                     f[x,y] .&.-                                                     ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.-                                                     (f[x,y] .&. g[x,y]) .&.-                                                     (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))]]))-{--[[<<forall x y.-      F(x,y) /\-      (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/-      (F(x,y) /\ G(x,y)) /\-      (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y))) >>]]--}-                                    (Set.map (Set.map render) (simpdnf (runSkolem (askolemize ((.~.) (generalize dpExampleFm))) :: Formula FOLEQ)))),-              TestCase (assertEqual "meson dp example, step 6 (p. 220)"-                                    (Set.map render-                                     (Set.fromList [for_all "x" . for_all "y" $-                                                    f[x,y] .&.-                                                    ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.-                                                    (f[x,y] .&. g[x,y]) .&.-                                                    (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))]))-{--[<<forall x y.-     F(x,y) /\-     (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/-     (F(x,y) /\ G(x,y)) /\ -     (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>]--}-                                    (Set.map render ((Set.map list_conj (simpdnf (runSkolem (askolemize ((.~.) (generalize dpExampleFm)))))) :: Set.Set (Formula FOLEQ))))]-    where f = pApp "F"-          g = pApp "G"-          sk1 = fApp (toSkolem "z")-          x = vt "x"-          y = vt "y"-          z = vt "z"--{--askolemize (simpdnf (generalize dpExampleFm)) ->- <<forall x y. F(x,y) /\ (~F(y,f_z(x,y)) \/ ~F(f_z(x,y), f_z(x,y))) \/ (F(x,y) /\ G(x,y)) /\ (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>--}
− Data/Logic/Tests/Harrison/Prop.hs 
@@ -1,404 +0,0 @@-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}-{-# OPTIONS_GHC -Wall -Wwarn #-}-module Data.Logic.Tests.Harrison.Prop-    ( tests-    ) where--import Data.Logic.Classes.Combine (Combinable(..), (∨), (∧))-import Data.Logic.Classes.Constants (true, false)-import Data.Logic.Classes.Formula (atomic)-import Data.Logic.Classes.Negate ((.~.), (¬))-import Data.Logic.Harrison.Lib ((|=>))-import Data.Logic.Harrison.Prop (eval, atoms, truthTable, tautology, pSubst, psimplify,-                                 nnf, dnf', rawdnf, dual, purednf, trivial, cnf')-import Data.Logic.Types.Harrison.Formulas.Propositional (Formula(..))-import Data.Logic.Types.Harrison.Prop (Prop(..))-import qualified Data.Map as Map-import qualified Data.Set as Set-import Prelude hiding (negate)-import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)---- main = runTestTT tests--tests :: Test-tests = TestLabel "Data.Logic.Tests.Harrison.Prop" $-        TestList [test01, test02, test03, test04, {-test05,-}-                  test06, test07, test08, test09, test10,-                  test11, test12, test13, test14, test15,-                  test16, test17, test18, test19, test20,-                  test21, test22, test23, test24, test25,-                  test26, test27, test28, test29, test30,-                  test31, test32, test33, test34, test35,-                  test36]---- Variables for use in test cases---- (p, q, r, s, t, u, v) = (Atom (P "p"), Atom (P "q"), Atom (P "r"), Atom (P "s"), Atom (P "t"), Atom (P "u"), Atom (P "v"))--test36 :: Test-test36 = TestCase $ assertEqual "show propositional formula 1" expected input-    where input = map show fms-          expected = ["((P \"p\") .&. (P \"q\")) .|. (P \"r\")",-                      "(P \"p\") .&. ((P \"q\") .|. (P \"r\"))",-                      "((P \"p\") .&. (P \"q\")) .|. (P \"r\")"]-          fms :: [Formula Prop]-          fms = [p .&. q .|. r, p .&. (q .|. r), (p .&. q) .|. r]-          (p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))---- ------------------------------------------------------------------------- --- Testing the parser and printer.                                           --- ------------------------------------------------------------------------- --test01 :: Test-test01 = TestCase $ assertEqual "Build Formula 1" expected input-    where input = (p .=>. q .<=>. r .&. s .|. (t .<=>. ((.~.) ((.~.) u)) .&. v))-          expected = (Iff-                      (Imp-                       (Atom (P {pname = "p"}))-                       (Atom (P {pname = "q"})))-                      (Or-                       (And (Atom (P {pname = "r"})) (Atom (P {pname = "s"})))-                       (Iff (Atom (P {pname = "t"}))-                        (And ({-Not-} ({-Not-} (Atom (P {pname = "u"})))) (Atom (P {pname = "v"}))))))-          (p, q, r, s, t, u, v) = (Atom (P "p"), Atom (P "q"), Atom (P "r"), Atom (P "s"), Atom (P "t"), Atom (P "u"), Atom (P "v"))--test02 :: Test-test02 = TestCase $ assertEqual "Build Formula 2" expected input-    where input = (Atom "fm" .&. Atom "fm")-          expected = (And (Atom "fm") (Atom "fm"))--test03 :: Test-test03 = TestCase $ assertEqual "Build Formula 3"-                                (Atom "fm" .|. Atom "fm" .&. Atom "fm")-                                (Or (Atom "fm") (And (Atom "fm") (Atom "fm")))---- ------------------------------------------------------------------------- --- Example of use.                                                           --- ------------------------------------------------------------------------- --test04 :: Test-test04 = TestCase $ assertEqual "fixity tests" expected input-    where (input, expected) = unzip (map (\ (fm, flag) -> (eval fm Map.empty, flag)) pairs)-          pairs :: [(Formula String, Bool)]-          pairs =-              [ ( true .&. false .=>. false .&. true,  True)-              , ( true .&. true  .=>. true  .&. false, False)-              , (   false ∧  true  ∨ true,             True)  -- "∧ binds more tightly than ∨"-              , (  (false ∧  true) ∨ true,             True)-              , (   false ∧ (true  ∨ true),            False)-              , (  (¬) true ∨ true,                    True)  -- "¬ binds more tightly than ∨"-              , (  (¬) (true ∨ true),                  False)-              ]---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test06 :: Test-test06 = TestCase $ assertEqual "atoms test" (atoms $ p .&. q .|. s .=>. ((.~.) p) .|. (r .<=>. s)) (Set.fromList [P "p",P "q",P "r",P "s"])-    where (p, q, r, s) = (Atom (P "p"), Atom (P "q"), Atom (P "r"), Atom (P "s"))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test07 :: Test-test07 = TestCase $ assertEqual "truth table 1 (p. 36)" expected input-    where input = (truthTable $ p .&. q .=>. q .&. r)-          expected =-              ([P "p", P "q", P "r"],-               [([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],False),-               ([True,True,True],True)])-          (p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))---- ------------------------------------------------------------------------- --- Additional examples illustrating formula classes.                         --- ------------------------------------------------------------------------- --test08 :: Test-test08 = TestCase $-    assertEqual "truth table 2 (p. 39)"-                (truthTable $  ((p .=>. q) .=>. p) .=>. p)-                ([P "p", P "q"],-                 [([False,False],True),-                  ([False,True],True),-                  ([True,False],True),-                  ([True,True],True)])-        where (p, q) = (Atom (P "p"), Atom (P "q"))--test09 :: Test-test09 = TestCase $-    assertEqual "truth table 3 (p. 40)" expected input-        where input = (truthTable $ p .&. ((.~.) p))-              expected = ([P "p"],-                          [([False],False),-                          ([True],False)])-              p = Atom (P "p")---- ------------------------------------------------------------------------- --- Examples.                                                                 --- ------------------------------------------------------------------------- --test10 :: Test-test10 = TestCase $ assertEqual "tautology 1 (p. 41)" True (tautology $ p .|. ((.~.) p)) where p = Atom (P "p")-test11 :: Test-test11 = TestCase $ assertEqual "tautology 2 (p. 41)" False (tautology $ p .|. q .=>. p) where (p, q) = (Atom (P "p"), Atom (P "q"))-test12 :: Test-test12 = TestCase $ assertEqual "tautology 3 (p. 41)" False (tautology $ p .|. q .=>. q .|. (p .<=>. q)) where (p, q) = (Atom (P "p"), Atom (P "q"))-test13 :: Test-test13 = TestCase $ assertEqual "tautology 4 (p. 41)" True (tautology $ (p .|. q) .&. ((.~.)(p .&. q)) .=>. ((.~.)p .<=>. q)) where (p, q) = (Atom (P "p"), Atom (P "q"))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test14 :: Test-test14 =-    TestCase $ assertEqual "pSubst (p. 41)" expected input-        where expected = (p .&. q) .&. q .&. (p .&. q) .&. q-              input = pSubst ((P "p") |=> (p .&. q)) (p .&. q .&. p .&. q)-              (p, q) = (Atom (P "p"), Atom (P "q"))---- ------------------------------------------------------------------------- --- Surprising tautologies including Dijkstra's "Golden rule".                --- ------------------------------------------------------------------------- --test15 :: Test-test15 = TestCase $ assertEqual "tautology 5 (p. 43)" expected input-    where input = tautology $ (p .=>. q) .|. (q .=>. p)-          expected = True-          (p, q) = (Atom (P "p"), Atom (P "q"))-test16 :: Test-test16 = TestCase $ assertEqual "tautology 6 (p. 45)" expected input-    where input = tautology $ p .|. (q .<=>. r) .<=>. (p .|. q .<=>. p .|. r)-          expected = True-          (p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))-test17 :: Test-test17 = TestCase $ assertEqual "Dijkstra's Golden Rule (p. 45)" expected input-    where input = tautology $ p .&. q .<=>. ((p .<=>. q) .<=>. p .|. q)-          expected = True-          (p, q) = (Atom (P "p"), Atom (P "q"))-test18 :: Test-test18 = TestCase $ assertEqual "Contraposition 1 (p. 46)" expected input-    where input = tautology $ (p .=>. q) .<=>. (((.~.)q) .=>. ((.~.)p))-          expected = True-          (p, q) = (Atom (P "p"), Atom (P "q"))-test19 :: Test-test19 = TestCase $ assertEqual "Contraposition 2 (p. 46)" expected input-    where input = tautology $ (p .=>. ((.~.)q)) .<=>. (q .=>. ((.~.)p))-          expected = True-          (p, q) = (Atom (P "p"), Atom (P "q"))-test20 :: Test-test20 = TestCase $ assertEqual "Contraposition 3 (p. 46)" expected input-    where input = tautology $ (p .=>. q) .<=>. (q .=>. p)-          expected = False-          (p, q) = (Atom (P "p"), Atom (P "q"))---- ------------------------------------------------------------------------- --- Some logical equivalences allowing elimination of connectives.            --- ------------------------------------------------------------------------- --test21 :: Test-test21 = TestCase $ assertEqual "Equivalences (p. 47)" expected input-    where input =-              map tautology-              [ true .<=>. false .=>. false-              , ((.~.)p) .<=>. p .=>. false-              , p .&. q .<=>. (p .=>. q .=>. false) .=>. false-              , p .|. q .<=>. (p .=>. false) .=>. q-              , (p .<=>. q) .<=>. ((p .=>. q) .=>. (q .=>. p) .=>. false) .=>. false ]-          expected = [True, True, True, True, True]-          (p, q) = (Atom (P "p"), Atom (P "q"))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test22 :: Test-test22 = TestCase $ assertEqual "Dual (p. 49)" expected input-    where input = dual (Atom (P "p") .|. ((.~.) (Atom (P "p"))))-          expected = And (Atom (P {pname = "p"})) (Not (Atom (P {pname = "p"})))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test23 :: Test-test23 = TestCase $ assertEqual "psimplify 1 (p. 50)" expected input-    where input = psimplify $ (true .=>. (x .<=>. false)) .=>. ((.~.) (y .|. false .&. z))-          expected = ((.~.) x) .=>. ((.~.) y)-          x = Atom (P "x")-          y = Atom (P "y")-          z = Atom (P "z")--test24 :: Test-test24 = TestCase $ assertEqual "psimplify 2 (p. 51)" expected input-    where input = psimplify $ ((x .=>. y) .=>. true) .|. (.~.) false-          expected = true-          x = Atom (P "x")-          y = Atom (P "y")---- ------------------------------------------------------------------------- --- Example of NNF function in action.                                        --- ------------------------------------------------------------------------- --test25 :: Test-test25 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input-    where input = nnf $ (p .<=>. q) .<=>. ((.~.)(r .=>. s))-          expected = Or (And (Or (And p q) (And (Not p) (Not q)))-                        (And r (Not s)))-                        (And (Or (And p (Not q)) (And (Not p) q))-                             (Or (Not r) s))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")-          s = Atom (P "s")--test26 :: Test-test26 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input-    where input = tautology (Iff fm fm')-          expected = True-          fm' = nnf fm-          fm = (p .<=>. q) .<=>. ((.~.)(r .=>. s))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")-          s = Atom (P "s")---- ------------------------------------------------------------------------- --- Some tautologies remarked on.                                             --- ------------------------------------------------------------------------- --test27 :: Test-test27 = TestCase $ assertEqual "tautology 1 (p. 53)" expected input-    where input = tautology $ (p .=>. p') .&. (q .=>. q') .=>. (p .&. q .=>. p' .&. q')-          expected = True-          p = Atom (P "p")-          q = Atom (P "q")-          p' = Atom (P "p'")-          q' = Atom (P "q'")-test28 :: Test-test28 = TestCase $ assertEqual "nnf 1 (p. 53)" expected input-    where input = tautology $ (p .=>. p') .&. (q .=>. q') .=>. (p .|. q .=>. p' .|. q')-          expected = True-          p = Atom (P "p")-          q = Atom (P "q")-          p' = Atom (P "p'")-          q' = Atom (P "q'")---- ------------------------------------------------------------------------- --- Examples.                                                                 --- ------------------------------------------------------------------------- --test29 :: Test-test29 = TestCase $ assertEqual "dnf 1 (p. 56)" expected input-    where input = (dnf' fm, truthTable fm)-          expected = (Or (And (Not r) p) (And r (And (Not p) q)),-                      ([P {pname = "p"}, P {pname = "q"}, P {pname = "r"}],-                       [([False,False,False],False),-                        ([False,False,True],False),-                        ([False,True,False],False),-                        ([False,True,True],True),-                        ([True,False,False],True),-                        ([True,False,True],False),-                        ([True,True,False],True),-                        ([True,True,True],False)]))-          fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")--test30 :: Test-test30 = TestCase $ assertEqual "dnf 2 (p. 56)" expected input-    where input = dnf' (p .&. q .&. r .&. s .&. t .&. u .|. u .&. v :: Formula Prop)-          expected = (v .&. u) .|. (q .&. (r .&. (s .&. (t .&. ((u .&. p))))))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")-          s = Atom (P "s")-          t = Atom (P "t")-          u = Atom (P "u")-          v = Atom (P "v")---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test31 :: Test-test31 = TestCase $ assertEqual "rawdnf (p. 58)" expected input-    where input = rawdnf $ (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          expected = ((atomic (P "p")) .&. ((.~.)(atomic (P "p"))) .|.-                      ((atomic (P "q")) .&. (atomic (P "r"))) .&. ((.~.)(atomic (P "p")))) .|.-                     ((atomic (P "p")) .&. ((.~.)(atomic (P "r"))) .|.-                      ((atomic (P "q")) .&. (atomic (P "r"))) .&. ((.~.)(atomic (P "r"))))-          (p, q, r) = (Atom (P "p"), Atom (P "q"), Atom (P "r"))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test32 :: Test-test32 = TestCase $ assertEqual "purednf (p. 58)" expected input-    where input = purednf $ (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          expected = Set.fromList [Set.fromList [p,Not p],-                                   Set.fromList [p,Not r],-                                   Set.fromList [q,r,Not p],-                                   Set.fromList [q,r,Not r]]-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test33 :: Test-test33 = TestCase $ assertEqual "trivial" expected input-    where input = Set.filter (not . trivial) (purednf fm)-          expected = Set.fromList [Set.fromList [p,Not r],-                                   Set.fromList [q,r,Not p]]-          fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test34 :: Test-test34 = TestCase $ assertEqual "dnf" expected input-    where input = (dnf' fm, tautology (Iff fm (dnf' fm)))-          expected = (Or (And (Not r) p) (And r (And (Not p) q)), True)-          fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test35 :: Test-test35 = TestCase $ assertEqual "cnf" expected input-    where input = (cnf' fm, tautology (Iff fm (cnf' fm)))-          -- Fully parenthesized-          -- expected = (((atomic (P "r")) .|. (atomic (P "p"))) .&. (((((.~.)(atomic (P "r")))) .|. (((.~.)(atomic (P "p"))))) .&. ((atomic (P "q")) .|. (atomic (P "p")))),True)-          -- Edited-          expected = (   ((atomic (P "r"))           .|. (atomic (P "p")))          .&.-                      (  (((.~.)(atomic (P "r")))   .|. ((.~.)(atomic (P "p"))))    .&.-                         ((atomic (P "q"))          .|. (atomic (P "p")))            ),-                      True)-          -- expected = (And (Or q p) (And (Or r p) (Or (Not r) (Not p))),True)-          -- expected = (F, True)-          -- expected = (((atomic (P "r")) .|. (atomic (P "p"))) .&. (((((.~.)(atomic (P "r"))))) .|. ((((.~.)(atomic (P "p"))))) .&. (atomic (P "q")) .|. (atomic (P "p"))),True)-          fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))-          p = Atom (P "p")-          q = Atom (P "q")-          r = Atom (P "r")
− Data/Logic/Tests/Harrison/Resolution.hs 
@@ -1,131 +0,0 @@-{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables #-}-{-# OPTIONS_GHC -Wall #-}-module Data.Logic.Tests.Harrison.Resolution where--import Control.Applicative.Error (Failing(..))-import Data.Logic.Classes.Combine (Combinable(..))-import Data.Logic.Classes.Equals (pApp)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))-import Data.Logic.Classes.Negate ((.~.))-import Data.Logic.Classes.Term (Term(vt, fApp))-import Data.Logic.Harrison.Normal (simpcnf)-import Data.Logic.Harrison.Resolution (resolution1, resolution2, resolution3, presolution)-import Data.Logic.Harrison.Skolem (runSkolem, skolemize)-import Data.Logic.Types.Harrison.Equal (FOLEQ)-import Data.Logic.Types.Harrison.FOL (Function(Skolem), TermType)-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula)-import qualified Data.Set as Set-import Data.String (IsString(..))-import Prelude hiding (negate)--- import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual, Assertion)-import Data.Logic.Tests.HUnit--tests :: Test (Formula FOLEQ)-tests = TestLabel "Data.Logic.Tests.Harrison.Resolution" $-        TestList [test01, test02, test03, test04, test05]---- ------------------------------------------------------------------------- --- Barber's paradox is an example of why we need factoring.                  --- ------------------------------------------------------------------------- --test01 :: Test (Formula FOLEQ)-test01 = TestCase $ assertEqual "Barber's paradox (p. 181)" expected input-    where input = simpcnf (runSkolem (skolemize id ((.~.)barb)))-          barb :: Formula FOLEQ-          barb = exists (fromString "b") (for_all (fromString "x") (shaves [b, x] .<=>. ((.~.)(shaves [x, x]))))-          -- This is not exactly what is in the book-          expected = Set.fromList [Set.fromList [shaves [b,     fx [b]], (.~.)(shaves [fx [b],fx [b]])],-                                   Set.fromList [shaves [fx [b],fx [b]], (.~.)(shaves [b,     fx [b]])]]-          x = vt (fromString "x")-          b = vt (fromString "b")-          fx = fApp (Skolem "x")-          shaves = pApp (fromString "shaves") ---- ------------------------------------------------------------------------- --- Simple example that works well.                                           --- ------------------------------------------------------------------------- --test02 :: Test (Formula FOLEQ)-test02 = TestCase $ assertEqual "Davis-Putnam example" expected input-    where input = runSkolem (resolution1 (dpExampleFm :: Formula FOLEQ))-          expected = Set.singleton (Success True)--dpExampleFm :: Formula FOLEQ-dpExampleFm = exists "x" . exists "y" .for_all "z" $-              (f [x, y] .=>. (f [y, z] .&. f [z, z])) .&.-              ((f [x, y] .&. g [x, y]) .=>. (g [x, z] .&. g [z, z]))-    where-      x = vt "x" :: TermType-      y = vt "y"-      z = vt "z"-      g = pApp "G" :: [TermType] -> Formula FOLEQ-      f = pApp "F"---- ------------------------------------------------------------------------- --- This is now a lot quicker.                                                --- ------------------------------------------------------------------------- --test03 :: Test (Formula FOLEQ)-test03 = TestCase $ assertEqual "Davis-Putnam example 2" expected input-    where input = runSkolem (resolution2 (dpExampleFm :: Formula FOLEQ))-          expected = Set.singleton (Success True)---- ------------------------------------------------------------------------- --- Example: the (in)famous Los problem.                                      --- ------------------------------------------------------------------------- --test04 :: Test (Formula FOLEQ)-test04 = TestCase $ assertEqual "Los problem (p. 198)" expected input-    where input = runSkolem (presolution losFm)-          expected = Set.fromList [Success True]--losFm :: Formula FOLEQ-losFm = (for_all x (for_all y (for_all z (p [vt x, vt y] .=>. p [vt y, vt z] .=>. p [vt x, vt z])))) .&.-        (for_all x (for_all y (for_all z (q [vt x, vt y] .=>. q [vt y, vt z] .=>. q [vt x, vt z])))) .&.-        (for_all x (for_all y (q [vt x, vt y] .=>. q [vt y, vt x]))) .&.-        (for_all x (for_all y (p [vt x, vt y] .|. q [vt x, vt y]))) .=>.-        (for_all x (for_all y (p [vt x, vt y]))) .|.-        (for_all x (for_all y (q [vt x, vt y])))-    where-      x = fromString "x"-      y = fromString "y"-      z = fromString "z"-      p = pApp (fromString "P")-      q = pApp (fromString "Q")--test05 :: Test (Formula FOLEQ)-test05 = TestCase $ assertEqual "Socrates syllogism" expected input-    where input = (runSkolem (resolution1 socrates),-                   runSkolem (resolution2 socrates),-                   runSkolem (resolution3 socrates),-                   runSkolem (presolution socrates),-                   runSkolem (resolution1 notSocrates),-                   runSkolem (resolution2 notSocrates),-                   runSkolem (resolution3 notSocrates),-                   runSkolem (presolution notSocrates))-          expected = (Set.singleton (Success True),-                      Set.singleton (Success True),-                      Set.singleton (Success True),-                      Set.singleton (Success True),-                      Set.singleton (Success {-False-} True),-                      Set.singleton (Success {-False-} True),-                      Set.singleton (Failure ["No proof found"]),-                      Set.singleton (Success {-False-} True))--socrates :: Formula FOLEQ-socrates =-    (for_all x (s [vt x] .=>. h [vt x]) .&. for_all x (h [vt x] .=>. m [vt x])) .=>. for_all x (s [vt x] .=>. m [vt x])-    where-      x = fromString "x"-      s = pApp (fromString "S")-      h = pApp (fromString "H")-      m = pApp (fromString "M")--notSocrates :: Formula FOLEQ-notSocrates =-    (for_all x (s [vt x] .=>. h [vt x]) .&. for_all x (h [vt x] .=>. m [vt x])) .=>. for_all x (s [vt x] .=>.  ((.~.)(m [vt x])))-    where-      x = fromString "x"-      s = pApp (fromString "S")-      h = pApp (fromString "H")-      m = pApp (fromString "M")
− Data/Logic/Tests/Harrison/Skolem.hs 
@@ -1,97 +0,0 @@-{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}-{-# OPTIONS_GHC -Wall #-}-module Data.Logic.Tests.Harrison.Skolem-    ( tests-    ) where--import Data.Logic.Classes.Combine (Combinable(..))-import Data.Logic.Classes.Constants (false)-import Data.Logic.Classes.Equals (pApp)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(exists, for_all))-import Data.Logic.Classes.Negate ((.~.))-import Data.Logic.Classes.Term (Term(..))-import Data.Logic.Harrison.Skolem (simplify, nnf, pnf)-import Data.Logic.Harrison.Skolem (runSkolem, skolemize)-import Data.Logic.Tests.HUnit ()-import Data.Logic.Types.Harrison.Equal (FOLEQ, PredName(..))-import Data.Logic.Types.Harrison.FOL (Function(..))-import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula)-import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)--tests :: Test-tests = TestLabel "Data.Logic.Tests.Harrison.Skolem" $ TestList [test01, test02, test03, test04, test05]---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test01 :: Test-test01 = TestCase $ assertEqual "simplify (p. 140)" expected input-    where p = Named "P"-          q = Named "Q"-          input = simplify fm-          expected = (for_all "x" (pApp p [vt "x"])) .=>. (pApp q []) :: Formula FOLEQ-          fm :: Formula FOLEQ-          fm = (for_all "x" (for_all "y" (pApp p [vt "x"] .|. (pApp p [vt "y"] .&. false)))) .=>. exists "z" (pApp q [])---- ------------------------------------------------------------------------- --- Example of NNF function in action.                                        --- ------------------------------------------------------------------------- --test02 :: Test-test02 = TestCase $ assertEqual "nnf (p. 140)" expected input-    where p = Named "P"-          q = Named "Q"-          input = nnf fm-          expected = exists "x" ((.~.)(pApp p [vt "x"])) .|.-                     ((exists "y" (pApp q [vt "y"]) .&. exists "z" ((pApp p [vt "z"]) .&. (pApp q [vt "z"]))) .|.-                      (for_all "y" ((.~.)(pApp q [vt "y"])) .&.-                       for_all "z" (((.~.)(pApp p [vt "z"])) .|. ((.~.)(pApp q [vt "z"])))))-          fm :: Formula FOLEQ-          fm = (for_all "x" (pApp p [vt "x"])) .=>. ((exists "y" (pApp q [vt "y"])) .<=>. exists "z" (pApp p [vt "z"] .&. pApp q [vt "z"]))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test03 :: Test-test03 = TestCase $ assertEqual "pnf (p. 144)" expected input-    where p = Named "P"-          q = Named "Q"-          r = Named "R"-          input = pnf fm-          expected = exists "x" (for_all "z"-                                 ((((.~.)(pApp p [vt "x"])) .&. ((.~.)(pApp r [vt "y"]))) .|.-                                  ((pApp q [vt "x"]) .|.-                                   (((.~.)(pApp p [vt "z"])) .|.-                                    ((.~.)(pApp q [vt "z"]))))))-          fm :: Formula FOLEQ-          fm = (for_all "x" (pApp p [vt "x"]) .|. (pApp r [vt "y"])) .=>.-               exists "y" (exists "z" ((pApp q [vt "y"]) .|. ((.~.)(exists "z" (pApp p [vt "z"] .&. pApp q [vt "z"])))))---- ------------------------------------------------------------------------- --- Example.                                                                  --- ------------------------------------------------------------------------- --test04 :: Test-test04 = TestCase $ assertEqual "skolemize 1 (p. 150)" expected input-    where input = runSkolem (skolemize id fm) :: Formula FOLEQ-          fm :: Formula FOLEQ-          fm = exists "y" (pApp (Named "<") [vt "x", vt "y"] .=>.-                           for_all "u" (exists "v" (pApp (Named "<") [fApp "*" [vt "x", vt "u"],  fApp "*" [vt "y", vt "v"]])))-          expected = ((.~.)(pApp (Named "<") [vt "x",fApp (Skolem "y") [vt "x"]])) .|.-                     (pApp (Named "<") [fApp "*" [vt "x",vt "u"],fApp "*" [fApp (Skolem "y") [vt "x"],fApp (Skolem "v") [vt "u",vt "x"]]])--test05 :: Test-test05 = TestCase $ assertEqual "skolemize 2 (p. 150)" expected input-    where p = Named "P"-          q = Named "Q"-          input = runSkolem (skolemize id fm) :: Formula FOLEQ-          fm :: Formula FOLEQ-          fm = for_all "x" ((pApp p [vt "x"]) .=>.-                            (exists "y" (exists "z" ((pApp q [vt "y"]) .|.-                                                     ((.~.)(exists "z" ((pApp p [vt "z"]) .&. (pApp q [vt "z"]))))))))-          expected = ((.~.)(pApp p [vt "x"])) .|.-                     ((pApp q [fApp (Skolem "y") []]) .|.-                      (((.~.)(pApp p [vt "z"])) .|.-                       ((.~.)(pApp q [vt "z"]))))
− Data/Logic/Tests/Harrison/Unif.hs 
@@ -1,46 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}-{-# OPTIONS_GHC -Wall -Wwarn #-}-module Data.Logic.Tests.Harrison.Unif-    ( tests-    ) where--import Data.Logic.Classes.Term (Term(fApp, vt), tsubst)-import Data.Logic.Failing (Failing(..), failing)-import Data.Logic.Harrison.Unif (fullUnify)-import Data.Logic.Tests.HUnit ()-import Data.Logic.Types.Harrison.FOL (TermType)-import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)--tests :: Test-tests = TestLabel "Data.Logic.Tests.Harrison.Unif" $ TestList [test01]---- ------------------------------------------------------------------------- --- Examples.                                                                 --- ------------------------------------------------------------------------- --test01 :: Test-test01 = TestCase $ assertEqual "Unify tests" expected input-    where input = map unify_and_apply eqss-          expected = map Success $-                      [[(fApp "f" [fApp "f" [vt "z"],fApp "g" [vt "y"]],-                        fApp "f" [fApp "f" [vt "z"],fApp "g" [vt "y"]])],-                      [(fApp "f" [vt "y",vt "y"],fApp "f" [vt "y",vt "y"])],-                      [(fApp "f" [fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]],-                                  fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]]],-                        fApp "f" [fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]],-                                  fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]]]),-                       (fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]],-                        fApp "f" [fApp "f" [vt "x3",vt "x3"],fApp "f" [vt "x3",vt "x3"]]),-                       (fApp "f" [vt "x3",vt "x3"],-                        fApp "f" [vt "x3",vt "x3"])]]-          unify_and_apply eqs =-              mapM app eqs-              where-                app (t1, t2) = failing Failure (\ i -> Success (tsubst i t1, tsubst i t2)) (fullUnify eqs)-          eqss :: [[(TermType, TermType)]]-          eqss =  [ [(fApp "f" [vt "x", fApp "g" [vt "y"]], fApp "f" [fApp "f" [vt "z"], vt "w"])]-                  , [(fApp "f" [vt "x", vt "y"], fApp "f" [vt "y", vt "x"])]-                  -- , [(fApp "f" [vt "x", fApp "g" [vt "y"]], fApp "f" [vt "y", vt "x"])] -- cyclic-                  , [(vt "x0", fApp "f" [vt "x1", vt "x1"]),-                     (vt "x1", fApp "f" [vt "x2", vt "x2"]),-                     (vt "x2", fApp "f" [vt "x3", vt "x3"])] ]
− Data/Logic/Tests/Logic.hs 
@@ -1,546 +0,0 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,-             ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances #-}-{-# OPTIONS -Wall -Wwarn -fno-warn-name-shadowing -fno-warn-orphans #-}-module Data.Logic.Tests.Logic (tests) where--import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..), (⇒))-import Data.Logic.Classes.Constants (Constants(..), true)-import Data.Logic.Classes.Equals (AtomEq, (.=.), pApp, pApp1, showAtomEq)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), showFirstOrder, (∀))-import Data.Logic.Classes.Atom (Atom)-import Data.Logic.Classes.Literal (Literal)-import Data.Logic.Classes.Negate (negated, (.~.))-import Data.Logic.Classes.Pretty (pretty)-import Data.Logic.Classes.Propositional (PropositionalFormula)-import Data.Logic.Classes.Skolem (Skolem(..))-import Data.Logic.Classes.Term (Term(..))-import Data.Logic.Classes.Variable (Variable)-import Data.Logic.Harrison.FOL (fv, subst, list_conj, list_disj)-import Data.Logic.Harrison.Normal (trivial)-import Data.Logic.Harrison.Prop (TruthTable, truthTable)-import Data.Logic.Harrison.Skolem (runSkolem, skolemize, pnf)-import Data.Logic.Normal.Clause (clauseNormalForm)-import Data.Logic.Normal.Implicative (runNormal)-import Data.Logic.Satisfiable (theorem, inconsistant)-import Data.Logic.Tests.Common (TFormula, TAtom, TTerm, myTest)-import Data.Logic.Types.FirstOrder-import qualified Data.Map as Map-import qualified Data.Set.Extra as Set-import Data.Set.Extra (fromList)-import Data.String (IsString(fromString))--- import PropLogic (PropForm(..), TruthTable, truthTable)-import qualified TextDisplay as TD-import Test.HUnit--tests :: Test-tests = TestLabel "Test.Logic" $ TestList [precTests, normalTests, theoremTests]--{--formCase :: (FirstOrderFormula TFormula TAtom V, AtomEq TAtom Pr TTerm, Term TTerm V AtomicFunction) =>-            String -> TFormula -> TFormula -> Test-formCase s expected input = TestLabel s $ TestCase (assertEqual s expected input)--}--precTests :: Test-precTests =-    TestList-    [ myTest "Logic - prec test 1"-               ((a .&. b) .|. c)-               (a .&. b .|. c)-      -- You can't apply .~. without parens:-      -- :type (.~. a)   -> (FormulaPF -> t) -> t-      -- :type ((.~.) a) -> FormulaPF-    , myTest "Logic - prec test 2"-               (((.~.) a) .&. b)-               ((.~.) a .&. b :: TFormula)-    -- 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.-    , myTest "Logic - prec test 3"-               ((a .&. b) .&. c) -- infixl, with infixr we get (a .&. (b .&. c))-               (a .&. b .&. c :: TFormula)-    , let x = vt "x" :: TTerm-          y = vt "y" :: TTerm-          -- This is not the desired result, but it is the result we-          -- will get due to the fact that function application-          -- precedence is always 10, and that rule applies when you-          -- put the operator in parentheses.  This means that direct-          -- input of examples from Harrison won't always work.-          expected = ((∀) "y" (pApp "g" [y])) ⇒ (pApp "f" [y]) :: TFormula-          input =     (∀) "y" (pApp "g" [y])  ⇒ (pApp "f" [y]) :: TFormula in-      myTest "Logic - prec test 4" expected input-    , TestCase (assertEqual "Logic - Find a free variable"-                (fv (for_all "x" (x .=. y) :: TFormula))-                (Set.singleton "y"))-{--    , let a = Combine (BinOp-                       (Combine (BinOp-                                 T-                                 (:=>:)-                                 (Combine (BinOp T (:&:) T))))-                       (:&:)-                       (Combine (BinOp-                                 (Combine (BinOp T (:&:) T))-                                 (:=>:)-                                 (Combine (BinOp T (:&:) T)))))-          b = Combine (BinOp-                       (Combine (BinOp-                                 T-                                 (:=>:)-                                 (Combine (BinOp-                                           (Combine (BinOp T (:&:) T))-                                           (:&:)-                                           (Combine (BinOp T (:&:) T))))))-                       (:=>:)-                       (Combine (BinOp T (:&:) T))) in-      ()--}-    , 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 = subst (Map.singleton (head . Set.toList . fv $ f) (vt "z")) f-      a = pApp ("a") []-      b = pApp ("b") []-      c = pApp ("c") []--x :: TTerm-x = vt (fromString "x")-y :: TTerm-y = vt (fromString "y")-z :: TTerm-z = vt (fromString "z")--normalTests =-    let s = pApp "S"-        h = pApp "H"-        m = pApp "M"-        x2 = vt "x2" :: TTerm-        for_all' x fm = for_all (fromString x) fm-        exists' x fm = exists (fromString x) fm-    in-    TestList-    [TestCase (assertEqual-               "nnf"-               (show (pretty (for_all' "x" (exists' "x2" ((s[x2] .&. ((.~.)(h[x2])) .|. h[x2] .&. ((.~.)(m[x2]))) .|. ((.~.)(s[x])) .|. m[x])) :: TFormula)))-               -- <<forall x. exists x'. (S(x') /\ ~H(x') \/ H(x') /\ ~M(x')) \/ ~S(x) \/ M(x)>>-               -- ∀x. ∃x2. ((S(x2) ∧ ¬H(x2) ∨ H(x2) ∧ ¬M(x2)) ∨ ¬S(x) ∨ M(x))-               (show-                (pretty-                 (pnf (((for_all' "x" (s[x] .=>. h[x])) .&. (for_all "x" (h[x] .=>. m[x]))) .=>.-                    (for_all "x" (s[x] .=>. m[x])) :: TFormula) :: TFormula))))]---- |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") [vt (V "x"),vt (V "y")])),-                         N (A (pApp ("f") [vt (V "z"),vt (V "x")])),-                         A (pApp ("f") [vt (V "z"),vt (V "y")])],-                     DJ [N (A (pApp ("q") [vt (V "x"),vt (V "y")])),-                         N (A (pApp ("f") [vt (V "z"),vt (V "y")])),-                         A (pApp ("f") [vt (V "z"),vt (V "x")])],-                     DJ [A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "x")]),-                         A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "y")]),-                         A (pApp ("q") [vt (V "x"),vt (V "y")])],-                     DJ [N (A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "y")])),-                         A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "y")]),-                         A (pApp ("q") [vt (V "x"),vt (V "y")])],-                     DJ [A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "x")]),-                         N (A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "x")])),-                         A (pApp ("q") [vt (V "x"),vt (V "y")])],-                     DJ [N (A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "y")])),-                         N (A (pApp ("f") [fApp (Skolem 1) [vt (V "x"),vt (V "y"),vt (V "z")],vt (V "x")])),-                         A (pApp ("q") [vt (V "x"),vt (V "y")])]]--moveQuantifiersOut1 :: Test-moveQuantifiersOut1 =-    myTest "Logic - moveQuantifiersOut1"-             (for_all "x2" ((pApp ("p") [vt ("x2")]) .&. ((pApp ("q") [vt ("x")]))))-             (prenexNormalForm (for_all "x" (pApp (fromString "p") [x]) .&. (pApp (fromString "q") [x])))--skolemize1 :: Test-skolemize1 =-    myTest "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 =-    myTest "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 =-    myTest "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 =-    myTest "Logic - inf1" expected formula-    where-      expected :: TFormula-      expected = ((pApp ("p") [vt ("x")]) .=>. (((pApp ("q") [vt ("x")]) .|. ((pApp ("r") [vt ("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)--}--theoremTests :: Test-theoremTests =-    let s = pApp "S"-        h = pApp "H"-        m = pApp "M"-        socrates1 = (for_all "x"   (s [x] .=>. h [x]) .&. for_all "x" (h [x] .=>. m [x]))  .=>.  for_all "x" (s [x] .=>. m [x])  :: TFormula -- First two clauses grouped - compare to 5-        socrates2 =  for_all "x" (((s [x] .=>. h [x]) .&.             (h [x] .=>. m [x]))  .=>.              (s [x] .=>. m [x])) :: TFormula -- shared binding for x-        socrates3 = (for_all "x"  ((s [x] .=>. h [x]) .&.             (h [x] .=>. m [x]))) .=>. (for_all "y" (s [y] .=>. m [y])) :: TFormula -- First two clauses share x, third is renamed y-        socrates5 =  for_all "x"   (s [x] .=>. h [x]) .&. for_all "x" (h [x] .=>. m [x])   .=>.  for_all "x" (s [x] .=>. m [x])  :: TFormula -- like 1, but less parens - check precedence -        socrates6 =  for_all "x"   (s [x] .=>. h [x]) .&. for_all "y" (h [y] .=>. m [y])   .=>.  for_all "z" (s [z] .=>. m [z])  :: TFormula -- Like 5, but with variables renamed-        socrates7 =  for_all "x"  ((s [x] .=>. h [x]) .&.             (h [x] .=>. m [x])   .&.               (m [x] .=>. ((.~.) (s [x])))) .&. (s [fApp "socrates" []]) in -    TestList-    [ myTest "Logic - theorem test 1"-                (True,(Set.empty, ([]{-Just (CJ [])-},[([],True)])))-                (runNormal (theorem socrates2), table socrates2)-    , myTest "Logic - theorem test 1a"-                (False,-                 False,-                 (fromList [fromList [Predicate (Apply "H" [FunApp (toSkolem "x") []]),-                                      Predicate (Apply "M" [Var "y"]),-                                      Predicate (Apply "S" [FunApp (toSkolem "x") []]),-                                      Combine ((:~:) (Predicate (Apply "S" [Var "y"])))],-                            fromList [Predicate (Apply "M" [Var "y"]),-                                      Predicate (Apply "S" [FunApp (toSkolem "x") []]),-                                      Combine ((:~:) (Predicate (Apply "M" [FunApp (toSkolem "x") []]))),-                                      Combine ((:~:) (Predicate (Apply "S" [Var "y"])))],-                            fromList [Predicate (Apply "M" [Var "y"]),-                                      Combine ((:~:) (Predicate (Apply "H" [FunApp (toSkolem "x") []]))),-                                      Combine ((:~:) (Predicate (Apply "M" [FunApp (toSkolem "x") []]))),-                                      Combine ((:~:) (Predicate (Apply "S" [Var "y"])))]],-                 ([(Apply "H" [fApp (toSkolem "x") []]),-                   (Apply "M" [vt ("y")]),-                   (Apply "M" [fApp (toSkolem "x") []]),-                   (Apply "S" [vt ("y")]),-                   (Apply "S" [fApp (toSkolem "x") []])],-                  [([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)])))-                -                (runNormal (theorem socrates3),-                 runNormal (inconsistant socrates3),-                 table socrates3)-    , myTest "socrates1 truth table"-             (let skx = fApp (toSkolem "x") in-              (fromList [fromList [Predicate (Apply "H" [FunApp (toSkolem "x") []]),-                                   Predicate (Apply "M" [Var "x"]),-                                   Predicate (Apply "S" [FunApp (toSkolem "x") []]),-                                   Combine ((:~:) (Predicate (Apply "S" [Var "x"])))],-                         fromList [Predicate (Apply "M" [Var "x"]),-                                   Predicate (Apply "S" [FunApp (toSkolem "x") []]),-                                   Combine ((:~:) (Predicate (Apply "M" [FunApp (toSkolem "x") []]))),-                                   Combine ((:~:) (Predicate (Apply "S" [Var "x"])))],-                         fromList [Predicate (Apply "M" [Var "x"]),-                                   Combine ((:~:) (Predicate (Apply "H" [FunApp (toSkolem "x") []]))),-                                   Combine ((:~:) (Predicate (Apply "M" [FunApp (toSkolem "x") []]))),-                                   Combine ((:~:) (Predicate (Apply "S" [Var "x"])))]],-              ([(Apply "H" [skx []]),-                (Apply "M" [x]),-                (Apply "M" [skx []]),-                (Apply "S" [x]),-                (Apply "S" [skx []])],-               -- Clauses are always true if x is not socrates-               -- Nothing,-               {- (Just (CJ [DJ [A (h[skx[]]), A (m[x]),     A (s[skx[]]), N (s[x])],  -- false when x is socrates and not mortal, and skx is socrates and human-                          DJ [A (m[x]),     A (s[skx[]]), N (A (m[skx[]])), N (s[x])],-                          DJ [A (m[x]),     N (A (h[x])), N (A (m[skx[]])), N (s[x])]])) -}-            --    h[skx] m[x] m[skx] s[x] s[skx]-               [([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)])))-                (table socrates1)--    , let skx = fApp (toSkolem "x")-          {- sky = fApp (toSkolem "y") -} in-      myTest "Socrates formula skolemized"-              -- ((s[skx []] .&. (.~.)(h[skx []]) .|. h[sky[]] .&. (.~.)(m[sky []])) .|. (.~.)(s[z]) .|. m[z])-                 ((s[skx []] .&. (.~.)(h[skx []]) .|. h[skx[]] .&. (.~.)(m[skx []])) .|. (.~.)(s[x]) .|. m[x])-                 (runSkolem (skolemize id socrates5) :: TFormula)--    , let skx = fApp (toSkolem "x")-          sky = fApp (toSkolem "y") in-      myTest "Socrates formula skolemized"-              -- ((s[skx []] .&. (.~.)(h[skx []]) .|. h[sky[]] .&. (.~.)(m[sky []])) .|. (.~.)(s[z]) .|. m[z])-                 ((s[skx []] .&. (.~.)(h[skx []]) .|. h[sky[]] .&. (.~.)(m[sky []])) .|. (.~.)(s[z]) .|. m[z])-                 (runSkolem (skolemize id socrates6) :: TFormula)--    , myTest "Logic - socrates is not mortal"-                (False,-                 False,-                 (fromList [fromList [Predicate (Apply "H" [Var "x"]),-                                      Combine ((:~:) (Predicate (Apply "S" [Var "x"])))],-                            fromList [Predicate (Apply "M" [Var "x"]),-                                      Combine ((:~:) (Predicate (Apply "H" [Var "x"])))],-                            fromList [Predicate (Apply "S" [FunApp "socrates" []])],-                            fromList [Combine ((:~:) (Predicate (Apply "M" [Var "x"]))),-                                      Combine ((:~:) (Predicate (Apply "S" [Var "x"])))]],-                 ([(Apply ("H") [vt ("x")]),-                   (Apply ("M") [vt ("x")]),-                   (Apply ("S") [vt ("x")]),-                   (Apply ("S") [fApp ("socrates") []])],-                  [([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") [vt ("x")]),((.~.) (pApp ("S") [vt ("x")]))],-                       [(pApp ("M") [vt ("x")]),((.~.) (pApp ("H") [vt ("x")]))],-                       [(pApp ("S") [fApp ("socrates") []])],-                       [((.~.) (pApp ("M") [vt ("x")])),((.~.) (pApp ("S") [vt ("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?-                (runNormal (theorem socrates7), runNormal (inconsistant socrates7), table socrates7, runNormal (clauseNormalForm socrates7) :: Set.Set (Set.Set TFormula))-    , let (formula :: TFormula) =-              (for_all "x" (pApp "L" [vt "x"] .=>. pApp "F" [vt "x"]) .&. -- All logicians are funny-               exists "x" (pApp "L" [vt "x"])) .=>.                            -- Someone is a logician-              (.~.) (exists "x" (pApp "F" [vt "x"]))                           -- Someone / Nobody is funny-          input = table formula-          expected = (fromList [fromList [Predicate (Apply "L" [FunApp (toSkolem "x") []]),-                                          Combine ((:~:) (Predicate (Apply "F" [Var "x2"]))),-                                          Combine ((:~:) (Predicate (Apply "L" [Var "x"])))],-                                fromList [Combine ((:~:) (Predicate (Apply "F" [Var "x2"]))),-                                          Combine ((:~:) (Predicate (Apply "F" [FunApp (toSkolem "x") []]))),-                                          Combine ((:~:) (Predicate (Apply "L" [Var "x"])))]],-                      ([(Apply ("F") [vt ("x2")]),-                       (Apply ("F") [fApp (toSkolem "x") []]),-                       (Apply ("L") [vt ("x")]),-                       (Apply ("L") [fApp (toSkolem "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 myTest "Logic - gensler189" expected input-    , let (formula :: TFormula) =-              (for_all "x" (pApp "L" [vt "x"] .=>. pApp "F" [vt "x"]) .&. -- All logicians are funny-               exists "y" (pApp "L" [vt (fromString "y")])) .=>.           -- Someone is a logician-              (.~.) (exists "z" (pApp "F" [vt "z"]))                       -- Someone / Nobody is funny-          input = table formula-          expected = (fromList [fromList [Predicate (Apply "L" [FunApp (toSkolem "x") []]),-                                          Combine ((:~:) (Predicate (Apply "F" [Var "z"]))),-                                          Combine ((:~:) (Predicate (Apply "L" [Var "y"])))],-                                fromList [Combine ((:~:) (Predicate (Apply "F" [Var "z"]))),-                                          Combine ((:~:) (Predicate (Apply "F" [FunApp (toSkolem "x") []]))),-                                          Combine ((:~:) (Predicate (Apply "L" [Var "y"])))]],-                      ([(Apply ("F") [vt ("z")]),-                       (Apply ("F") [fApp (toSkolem "x") []]),-                       (Apply ("L") [vt ("y")]),-                       (Apply ("L") [fApp (toSkolem "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 myTest "Logic - gensler189 renamed" expected input-    ]--toSS :: Ord a => [[a]] -> Set.Set (Set.Set a)-toSS = Set.fromList . map Set.fromList--{--theorem5 =-    myTest "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 showAtomEq 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) =-    ( myTest "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--}-         {- forall formula atom term v p f.-         (FirstOrderFormula formula atom v,-          PropositionalFormula formula atom,-          Atom atom term v,-          AtomEq atom p term,-          Constants p, Eq p, Term term v f, Literal formula atom v,-          Ord formula, Skolem f v, IsString v, Variable v, TD.Display formula) => -}--table :: forall formula atom term v f.-         (FirstOrderFormula formula atom v,-          PropositionalFormula formula atom,-          Literal formula atom,-          Atom atom term v,-          Term term v f,-          Ord formula, Ord atom) =>-         formula -> (Set.Set (Set.Set formula), TruthTable atom)-table f =-    -- truthTable :: Ord a => PropForm a -> TruthTable a-    (cnf, truthTable cnf')-    where-      cnf' :: formula-      cnf' = list_conj (Set.map list_disj cnf :: Set.Set formula) -- CJ (map (DJ . map n) cnf)-      cnf :: Set.Set (Set.Set formula)-      cnf = runNormal (clauseNormalForm f)-      fromSS = map Set.toList . Set.toList-      -- n f = (if negated f then (.~.) . atomic . (.~.) else atomic) $ f-      -- list_disj = setFoldr1 (.|.)-      -- list_conj = setFoldr1 (.&.)--setFoldr1 :: (a -> a -> a) -> Set.Set a -> a-setFoldr1 f s =-    case Set.minView s of-      Nothing -> error "setFoldr1"-      Just (x, s') -> Set.fold f x s'
Data/Logic/Tests/Main.hs view
@@ -1,13 +1,13 @@-import Data.Logic.Tests.Common (TestFormula, TestProof, V, TFormula, TAtom, TTerm)+import Common (TestFormula, TestProof, V, TFormula, TAtom, TTerm) import System.Exit import Test.HUnit import qualified Data.Logic.Harrison.DP as DP import qualified Data.Logic.Harrison.PropExamples as PropExamples-import qualified Data.Logic.Tests.Harrison.Main as Harrison-import qualified Data.Logic.Tests.Logic as Logic-import qualified Data.Logic.Tests.Chiou0 as Chiou0+import qualified Harrison.Main as Harrison+import qualified Logic+import qualified Chiou0 as Chiou0 --import qualified Data.Logic.Tests.TPTP as TPTP-import qualified Data.Logic.Tests.Data as Data+import qualified Data  main :: IO () main =
− Data/Logic/Tests/TPTP.hs 
@@ -1,22 +0,0 @@-module Data.Logic.Tests.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 "Test.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)
changelog view
@@ -1,3 +1,9 @@+haskell-logic-classes (1.5.1) unstable; urgency=low++  * Update Homepage and Bug-Reports fields in cabal file++ -- David Fox <dsf@seereason.com>  Mon, 13 Apr 2015 14:16:10 -0700+ haskell-logic-classes (1.5) unstable; urgency=low    * Move the pApp* functions from Data.Logic.Classes.FirstOrder to
logic-classes.cabal view
@@ -1,17 +1,17 @@ Name:             logic-classes-Version:          1.5+Version:          1.5.1 Synopsis:         Framework for propositional and first order logic, theorem proving 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                   several logic algorithms, including conversion to normal form and a simple                   resolution-based theorem prover for any instance of FirstOrderFormula.-Homepage:         http://src.seereason.com/logic-classes+Homepage:         https://github.com/seereason/logic-classes License:          BSD3 License-File:     COPYING Author:           David Fox <dsf@seereason.com> Maintainer:       SeeReason Partners <partners@seereason.com>-Bug-Reports:      http://bugzilla.seereason.com/+Bug-Reports:      https://github.com/seereason/logic-classes/issues Category:         Logic, Theorem Provers Cabal-version:    >= 1.9 Build-Type:       Simple@@ -53,7 +53,8 @@                    Data.Logic.Harrison.Skolem                    Data.Logic.Harrison.Tableaux                    Data.Logic.Harrison.Unif-                   -- Data.Logic.Instances.Chiou+                   Data.Logic.HUnit+                   Data.Logic.Instances.Chiou                    Data.Logic.Instances.PropLogic                    Data.Logic.Instances.SatSolver                    -- Data.Logic.Instances.TPTP@@ -62,7 +63,6 @@                    Data.Logic.Normal.Implicative                    Data.Logic.Resolution                    Data.Logic.Satisfiable-                   Data.Logic.Tests.HUnit                    Data.Logic.Types.Common                    Data.Logic.Types.FirstOrder                    Data.Logic.Types.FirstOrderPublic@@ -74,25 +74,11 @@                    Data.Logic.Types.Propositional                    Data.Boolean                    Data.Boolean.SatSolver- Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit,-                   mtl, syb-with-class, text, PropLogic >= 0.9.0.3, pretty, safecopy, set-extra, syb, template-haskell+ Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, HUnit, mtl, pretty, PropLogic, safecopy, set-extra, syb, template-haskell -Executable tests+Test-Suite logic-classes-tests+ Type: exitcode-stdio-1.0  GHC-Options: -Wall -O2- Main-Is: Data/Logic/Tests/Main.hs- Build-Depends: applicative-extras, base, containers, HUnit, mtl,-                pretty, PropLogic, safecopy, set-extra, syb, template-haskell- Other-Modules:    Data.Logic.Tests.Chiou0-                   Data.Logic.Tests.Common-                   Data.Logic.Tests.Data-                   Data.Logic.Tests.Logic-                   Data.Logic.Tests.TPTP-                   Data.Logic.Tests.Harrison.Common-                   Data.Logic.Tests.Harrison.Equal-                   Data.Logic.Tests.Harrison.FOL-                   Data.Logic.Tests.Harrison.Meson-                   Data.Logic.Tests.Harrison.Prop-                   Data.Logic.Tests.Harrison.Resolution-                   Data.Logic.Tests.Harrison.Skolem-                   Data.Logic.Tests.Harrison.Main-                   Data.Logic.Tests.Harrison.Unif+ Hs-Source-Dirs: Data/Logic/Tests+ Main-Is: Main.hs+ Build-Depends: applicative-extras, base, containers, HUnit, logic-classes, mtl, pretty, PropLogic, set-extra, syb