logic-classes 1.7 → 1.7.1
raw patch · 19 files changed
+3445/−6 lines, 19 filessetup-changed
Files
- Data/Logic/Classes/Atom.hs +1/−1
- Data/Logic/Types/FirstOrder.hs +1/−1
- Setup.hs +1/−2
- Tests/Chiou0.hs +111/−0
- Tests/Common.hs +212/−0
- Tests/Data.hs +1138/−0
- Tests/Harrison/Common.hs +10/−0
- Tests/Harrison/Equal.hs +251/−0
- Tests/Harrison/FOL.hs +221/−0
- Tests/Harrison/Main.hs +29/−0
- Tests/Harrison/Meson.hs +122/−0
- Tests/Harrison/Prop.hs +404/−0
- Tests/Harrison/Resolution.hs +129/−0
- Tests/Harrison/Skolem.hs +89/−0
- Tests/Harrison/Unif.hs +46/−0
- Tests/Logic.hs +636/−0
- Tests/TPTP.hs +22/−0
- changelog +6/−0
- logic-classes.cabal +16/−2
Data/Logic/Classes/Atom.hs view
@@ -8,7 +8,7 @@ -- , Formula(..) ) where -import Control.Applicative.Error (Failing)+import Data.Logic.ATP (Failing) import qualified Data.Map as Map import qualified Data.Set as Set
Data/Logic/Types/FirstOrder.hs view
@@ -13,7 +13,7 @@ import Data.Logic.ATP.FOL (IsFirstOrder) import Data.Logic.ATP.Formulas (IsAtom, IsFormula(..)) import Data.Logic.ATP.Lit (IsLiteral(..))-import Data.Logic.ATP.Pretty (HasFixity(..), Pretty(pPrint, pPrintPrec), Side(Top))+import Data.Logic.ATP.Pretty (HasFixity(..), Pretty(pPrintPrec), Side(Top)) import Data.Logic.ATP.Prop (BinOp(..), IsPropositional(..)) import Data.Logic.ATP.Quantified (associativityQuantified, exists, IsQuantified(..), precedenceQuantified, prettyQuantified, Quant(..)) import Data.Logic.ATP.Term (IsFunction, IsTerm(..), IsVariable(..), prettyTerm, V)
Setup.hs view
@@ -6,5 +6,4 @@ import System.Directory (copyFile) main :: IO ()-main = copyFile "debian/changelog" "changelog" >>- defaultMainWithHooks simpleUserHooks+main = defaultMainWithHooks simpleUserHooks
+ Tests/Chiou0.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, StandaloneDeriving, TypeSynonymInstances #-}+{-# OPTIONS -fno-warn-orphans #-}++module Chiou0 where++import Common ({-instance Atom MyAtom MyTerm V-})+import Control.Monad.Trans (MonadIO, liftIO)+import Data.Logic.ATP.Apply (pApp)+import Data.Logic.ATP.Lit ((.~.), IsLiteral(..), LFormula)+import Data.Logic.ATP.Pretty (assertEqual')+import Data.Logic.ATP.Prop (IsPropositional(..))+import Data.Logic.ATP.Quantified (exists, for_all)+import Data.Logic.ATP.Skolem (HasSkolem(..), SkolemT, SkAtom)+import Data.Logic.ATP.Term (IsTerm(..))+import Data.Logic.Instances.Test (V(..), Function(..), TFormula, TTerm)+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.Map (fromList)+import qualified Data.Set as S+import Test.HUnit++tests :: Test+tests = TestLabel "Test.Chiou0" $ TestList [loadTest, proofTest1, proofTest2]++loadTest :: Test+loadTest =+ let label = "Chiuo0 - loadKB test" in+ TestLabel label (TestCase (assertEqual' label expected (runProver' Nothing (loadKB sentences))))+ where+ expected :: [Proof (LFormula SkAtom)]+ expected = [Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem "x" 1) []])]),+ makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x" 1) []])])]),+ Proof Invalid (S.fromList [makeINF' ([(pApp ("Dog") [vt ("y'")]),(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 = let label = "Chiuo0 - proof test 1" in+ TestLabel label (TestCase (assertEqual' label proof1 (runProver' Nothing (loadKB sentences >> theoremKB (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula)))))++inf' :: (IsLiteral lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit+inf' l1 l2 = INF (S.fromList l1) (S.fromList l2)++proof1 :: (Bool, SetOfSupport (LFormula SkAtom) 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 ("y'")]),(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 ("y'")]),(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 ("y'")]),(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Owns") [fApp ("Curiosity") [],vt ("y")])]) ([]),fromList [])]))++proofTest2 :: Test+proofTest2 = let label = "Chiuo0 - proof test 2" in+ TestLabel label (TestCase (assertEqual' label proof2 (runProver' Nothing (loadKB sentences >> theoremKB conjecture))))+ where+ conjecture :: TFormula+ conjecture = (pApp "Kills" [fApp "Curiosity" [], fApp (Fn "Tuna") []])++proof2 :: (Bool, SetOfSupport (LFormula SkAtom) 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 ("y'")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y'")]),(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 ("y'")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y'")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Dog") [vt ("y'")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),fromList []),+ (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])++testProof :: MonadIO m =>+ String+ -> (TFormula, Bool, (S.Set (ImplicativeForm (LFormula SkAtom))))+ -> ProverT (ImplicativeForm (LFormula SkAtom)) (SkolemT m Function) ()+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 (LFormula SkAtom)) (SkolemT m Function) [Proof (LFormula SkAtom)]+loadCmd = loadKB sentences++-- instance IsAtom (Predicate Pr (PTerm V Function))++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"]))]
+ Tests/Common.hs view
@@ -0,0 +1,212 @@+-- |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 CPP, DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes,+ ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wwarn #-}+module Common+ ( render+ , TestFormula(..)+ , Expected(..)+ , doTest+ , TestProof(..)+ , TTestProof+ , ProofExpected(..)+ , doProof+ ) where++import Control.Monad.Identity (Identity)+import Control.Monad.Reader (MonadPlus(..), msum)+import qualified Data.Boolean as B (CNF, Literal)+import Data.Generics (Data, Typeable, listify)+import Data.List as List (map, null)+import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), Predicate)+import Data.Logic.ATP.Equate (HasEquate(foldEquate))+import Data.Logic.ATP.FOL (asubst, fva, IsFirstOrder)+import Data.Logic.ATP.Formulas (IsFormula(AtomOf))+import Data.Logic.ATP.Lit (convertLiteral, LFormula)+import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint))+import Data.Logic.ATP.Prop (convertPropositional, PFormula, satisfiable, trivial)+import Data.Logic.ATP.Quantified (convertQuantified, IsQuantified(..))+import Data.Logic.ATP.Skolem (Function, SkAtom, SkTerm, SkolemT, Formula, simpcnf', simpdnf', HasSkolem(SVarOf),+ nnf, pnf, runSkolem, simplify, skolemize, skolems)+import Data.Logic.ATP.Term (fApp, foldTerm, IsTerm(FunOf, TVarOf), V, vt)+import Data.Logic.Classes.Atom (Atom(..))+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 (ProverT')+import Data.Logic.KnowledgeBase (WithId, runProver', Proof, loadKB, theoremKB, getKB)+import Data.Logic.Normal.Implicative (ImplicativeForm, runNormal, runNormalT)+import Data.Logic.Resolution (getSubstAtomEq, isRenameOfAtomEq, SetOfSupport)+import Data.Set as Set+import PropLogic (PropForm)+import Test.HUnit+import Text.PrettyPrint (Style(mode), renderStyle, style, Mode(OneLineMode))++instance Atom SkAtom SkTerm V where+ substitute = asubst+ freeVariables = fva+ allVariables = fva -- Variables are always free in an atom - this method is unnecessary+ unify = unify+ match = unify+ foldTerms f r pr = foldEquate (\t1 t2 -> f t2 (f t1 r)) (\_ ts -> Prelude.foldr f r ts) pr+ isRename = isRenameOfAtomEq+ getSubst = getSubstAtomEq++instance IsFirstOrder (PropForm SkAtom)++-- | We shouldn't need this instance, but right now we need ot to use+-- convertFirstOrder. The conversion functions need work.+instance IsQuantified (PropForm SkAtom) where+ type VarOf (PropForm SkAtom) = V+ quant _ _ _ = error "FIXME: IsQuantified (PropForm SkAtom) SkAtom V"+ foldQuantified = error "FIXME: IsQuantified (PropForm SkAtom) SkAtom V"++-- | Render a Pretty instance in single line mode+render :: Pretty a => a -> String+render = renderStyle (style {mode = OneLineMode}) . pPrint++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 (PFormula SkAtom)+ | SkolemNumbers (Set Function)+ | ClauseNormalForm (Set (Set (LFormula atom)))+ | DisjNormalForm (Set (Set (LFormula atom)))+ | TrivialClauses [(Bool, (Set formula))]+ | ConvertToChiou (Ch.Sentence V Predicate Function)+ | ChiouKB1 (Proof (LFormula atom))+ | PropLogicSat Bool+ | SatSolverCNF B.CNF+ | SatSolverSat Bool+ -- deriving (Data, Typeable)++type TTestFormula = TestFormula Formula SkAtom V++doTest :: TTestFormula -> Test+doTest (TestFormula fm nm expect) =+ TestLabel nm $ TestList $+ List.map doExpected expect+ where+ doExpected :: Expected Formula SkAtom V -> Test+ doExpected (FirstOrderFormula f') = let label = (nm ++ " original formula") in TestLabel label (TestCase (assertEqual' label f' fm))+ doExpected (SimplifiedForm f') = let label = (nm ++ " simplified") in TestLabel label (TestCase (assertEqual' label f' (simplify fm)))+ doExpected (PrenexNormalForm f') = let label = (nm ++ " prenex normal form") in TestLabel label (TestCase (assertEqual' label f' (pnf fm)))+ doExpected (NegationNormalForm f') = let label = (nm ++ " negation normal form") in TestLabel label (TestCase (assertEqual' label f' (nnf . simplify $ fm)))+ doExpected (SkolemNormalForm f') = let label = (nm ++ " skolem normal form") in TestLabel label (TestCase (assertEqual' label f' (runSkolem (skolemize id fm :: SkolemT Identity Function (PFormula SkAtom)))))+ doExpected (SkolemNumbers f') = let label = (nm ++ " skolem numbers") in TestLabel label (TestCase (assertEqual' label f' (skolems (runSkolem (skolemize id fm :: SkolemT Identity Function (PFormula SkAtom))))))+ doExpected (ClauseNormalForm fss) =+ let label = (nm ++ " clause normal form") in+ TestLabel label (TestCase (assertEqual' label+ ((List.map (List.map (convertLiteral id)) . Set.toList . Set.map Set.toList $ fss) :: [[Formula]])+ ((Set.toList . Set.map (Set.toList) . simpcnf' . (convertPropositional id :: PFormula SkAtom -> Formula) . runSkolem . skolemize id $ fm) :: [[Formula]])))+ where+ convert :: PFormula SkAtom -> Formula+ convert = undefined -- ((convertLiteral id) :: LFormula SkAtom -> Formula)+ doExpected (DisjNormalForm fss) =+ let label = (nm ++ " disjunctive normal form") in+ TestLabel label (TestCase (assertEqual' label+ ((List.map (List.map (convertLiteral id)) . Set.toList . Set.map Set.toList $ fss) :: [[Formula]])+ ((Set.toList . Set.map (Set.toList) . simpdnf' . (convertPropositional id :: PFormula SkAtom -> Formula) . runSkolem . skolemize id $ fm) :: [[Formula]])))+ doExpected (TrivialClauses flags) = let label = (nm ++ " trivial clauses") in TestLabel label (TestCase (assertEqual' label flags (List.map (\ (x :: Set Formula) -> (trivial x, x)) (Set.toList (simpcnf' (fm :: Formula))))))+ doExpected (ConvertToChiou result) =+ -- We need to convert formula to Chiou and see if it matches result.+ let ca :: SkAtom -> Ch.Sentence V Predicate Function+ -- ca = undefined+ ca = foldEquate (\t1 t2 -> Ch.Equal (ct t1) (ct t2)) (\p ts -> Ch.Predicate p (List.map ct ts))+ ct :: SkTerm -> Ch.CTerm V Function+ ct = foldTerm cv fn+ cv :: V -> Ch.CTerm V Function+ cv = vt+ fn :: Function -> [SkTerm] -> Ch.CTerm V Function+ fn f ts = fApp f (List.map ct ts) in+ let label = (nm ++ " converted to Chiou") in TestLabel label (TestCase (assertEqual' label result (convertQuantified ca id fm :: Ch.Sentence V Predicate Function)))+ doExpected (ChiouKB1 result) = let label = (nm ++ " Chiou KB") in TestLabel label (TestCase (assertEqual' label result ((runProver' Nothing (loadKB [fm] >>= return . head)) :: (Proof (LFormula SkAtom)))))+ doExpected (PropLogicSat result) = let label = (nm ++ " PropLogic.satisfiable") in TestLabel label (TestCase (assertEqual' label result (plSat (runSkolem (skolemize id fm)))))+ doExpected (SatSolverCNF result) = let label = (nm ++ " SatSolver CNF") in TestLabel label (TestCase (assertEqual' label (norm result) (runNormal (SS.toCNF fm))))+ doExpected (SatSolverSat result) = let label = (nm ++ " SatSolver CNF") in TestLabel label (TestCase (assertEqual' label result ((List.null :: [a] -> Bool) (runNormalT (SS.toCNF fm >>= return . satisfiable)))))++-- p = id++norm :: [[B.Literal]] -> [[B.Literal]]+norm = List.map Set.toList . Set.toList . Set.fromList . List.map Set.fromList++-- | @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 . List.map return . listify (const True)++data TestProof fof atom term v+ = TestProof+ { proofName :: String+ , proofKnowledge :: (String, [fof])+ , conjecture :: fof+ , proofExpected :: [ProofExpected (LFormula atom) v term]+ } deriving (Data, Typeable)++type TTestProof = TestProof Formula SkAtom SkTerm V++data ProofExpected lit v term+ = ChiouResult (Bool, SetOfSupport lit v term)+ | ChiouKB (Set (WithId (ImplicativeForm lit)))+ deriving (Data, Typeable)++doProof :: forall formula lit atom term v function.+ (IsFirstOrder formula, Ord formula, Pretty formula,+ lit ~ LFormula atom,+ HasEquate atom,+ Atom atom term v,+ HasSkolem function,+ Eq formula, Eq term, Eq v, Ord term, Show formula, Show term, Show v,+ Data lit, Data atom, Data formula, Typeable function,+ atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,+ v ~ TVarOf term, v ~ SVarOf function) =>+ TestProof formula atom term v -> Test+doProof p =+ TestLabel (proofName p) $ TestList $+ concatMap doExpected (proofExpected p)+ where+ doExpected :: ProofExpected lit v term -> [Test]+ doExpected (ChiouResult result) =+ [let label = (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " using Chiou prover") in+ TestLabel label (TestCase (assertEqual' label result (runProver' Nothing (loadKB' kb >> theoremKB' c))))]+ doExpected (ChiouKB result) =+ [let label = (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " Chiou knowledge base") in+ TestLabel label (TestCase (assertEqual label result (runProver' Nothing (loadKB kb >> getKB))))]+ kb = snd (proofKnowledge p) :: [formula]+ c = conjecture p :: formula++loadKB' :: forall m formula lit atom p term v f.+ (atom ~ AtomOf formula, v ~ TVarOf term, v ~ SVarOf f, term ~ TermOf atom, p ~ PredOf atom, f ~ FunOf term,+ lit ~ LFormula atom,+ Monad m, Data formula, Data atom,+ IsFirstOrder formula, Ord formula, Pretty formula,+ HasEquate atom,+ HasSkolem f,+ Atom atom term v,+ IsTerm term, Typeable f) => [formula] -> ProverT' v term lit m [Proof lit]+loadKB' = loadKB++theoremKB' :: forall m formula lit atom p term v f.+ (atom ~ AtomOf formula, v ~ TVarOf term, v ~ SVarOf f, term ~ TermOf atom, p ~ PredOf atom, f ~ FunOf term,+ lit ~ LFormula atom,+ Monad m, Data formula, Data atom,+ IsFirstOrder formula, Ord formula, Pretty formula,+ HasEquate atom,+ HasSkolem f,+ Atom atom term v,+ IsTerm term, Typeable f+ ) => formula -> ProverT' v term lit m (Bool, SetOfSupport lit v term)+theoremKB' = theoremKB
+ Tests/Data.hs view
@@ -0,0 +1,1138 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction #-}+{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}+{-# OPTIONS -fno-warn-name-shadowing #-}+module Data+ ( tests+ , allFormulas+ , proofs+{-+ , formulas+ , animalKB+ , animalConjectures+ , chang43KB+ , chang43Conjecture+ , chang43ConjectureRenamed+-}+ ) where++import Common (TestFormula(..), TestProof(..), Expected(..), ProofExpected(..), doTest, doProof, TTestProof)+import Data.Boolean (Literal(..))+import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), pApp, Predicate)+import Data.Logic.ATP.Equate ((.=.), HasEquate)+import Data.Logic.ATP.Formulas (false, IsFormula(AtomOf), true)+import Data.Logic.ATP.Lit ((.~.), IsLiteral)+import Data.Logic.ATP.Prop (IsPropositional(..))+import Data.Logic.ATP.Quantified (IsQuantified(..), for_all, exists)+import Data.Logic.ATP.Skolem (HasSkolem(toSkolem), Formula, SkAtom, SkTerm, Function)+import Data.Logic.ATP.Term (IsTerm(..), V)+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.Map as Map (fromList)+import Data.Set as Set (Set, fromList, toList)+import Data.String (IsString)+import Test.HUnit+import Text.PrettyPrint.HughesPJClass (prettyShow)++-- |for_all with a list of variables, for backwards compatibility.+for_all' :: IsQuantified formula => [VarOf formula] -> formula -> formula+for_all' vs f = foldr for_all f vs++-- |exists with a list of variables, for backwards compatibility.+exists' :: IsQuantified formula => [VarOf formula] -> formula -> formula+exists' vs f = foldr for_all f vs++pApp2 :: (atom ~ AtomOf formula, term ~ TermOf atom, p ~ PredOf atom,+ IsFormula formula, HasApply atom) => p -> term -> term -> formula+pApp2 p a b = pApp p [a, b]++{-+:m +Data.Logic.Test+:m +Data.Logic.Types.FirstOrder+:m +Data.Set+runNormal (clauseNormalForm (true :: Formula V Predicate Function)) :: Set (Set (Formula V Predicate Function))+runNormal (skolemNormalForm (true :: Formula V Predicate Function)) :: Formula V Predicate Function+:m +Data.Logic.Normal.Prenex+prenexNormalForm true :: Formula V Predicate Function+:m +Data.Logic.Normal.Skolem+:m +Data.Logic.Normal.Negation+-}++tests :: [Test] -> [TTestProof] -> Test+tests fs ps =+ TestLabel "Tests.Data" $ TestList (fs ++ map doProof ps)++allFormulas :: [Test]+allFormulas = (formulas +++ map doTest (concatMap snd [animalKB, chang43KB]) +++ animalConjectures +++ [chang43Conjecture, chang43ConjectureRenamed])++formulas :: [Test]+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" :: SkTerm, vt "y" :: SkTerm, vt "z" :: SkTerm, vt "u" :: SkTerm, vt "v" :: SkTerm, vt "w" :: SkTerm)+ z2 = vt "z'" :: SkTerm in+ [ doTest $+ TestFormula+ { formula = p0 .|. q0 .&. r0 .|. n s0 .&. n t0+ , name = "operator precedence"+ , expected = [ FirstOrderFormula (p0 .|. (q0 .&. r0) .|. ((n s0) .&. (n t0))) ] }+ , doTest $+ TestFormula+ { formula = true+ , name = "True"+ , expected = [ClauseNormalForm (toSS [[]])] }+ , doTest $+ TestFormula+ { formula = false+ , name = "False"+ , expected = [ClauseNormalForm (toSS [])] }+ , doTest $+ TestFormula+ { formula = true+ , name = "True"+ , expected = [DisjNormalForm (toSS [[]])] } -- Make sure these are right+ , doTest $+ TestFormula+ { formula = false+ , name = "False"+ , expected = [DisjNormalForm (toSS [])] }+ , doTest $+ TestFormula+ { formula = pApp "p" []+ , name = "p"+ , expected = [ClauseNormalForm (toSS [[pApp "p" []]])] }+ , let p = pApp "p" [] in+ doTest $+ TestFormula+ { formula = p .&. ((.~.) (p))+ , name = "p&~p"+ , expected = [ PrenexNormalForm ((pApp ("p") []) .&. (((.~.) (pApp ("p") []))))+ , ClauseNormalForm (toSS [[(p)], [((.~.) (p))]])+ ] }+ , doTest $+ TestFormula+ { formula = pApp "p" [vt "x"]+ , name = "p[x]"+ , expected = [ClauseNormalForm (toSS [[pApp "p" [x]]])] }+ , let f = pApp "f"+ q = pApp "q" in+ doTest $+ 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 "z'"+ (((((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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("y"))),+ (pApp2 ("q") (vt ("x")) (vt ("y")))],+ [(pApp2 ("q") (vt ("x")) (vt ("y"))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("y"))))]])+ ]+ }+ , doTest $+ TestFormula+ { name = "move quantifiers out"+ , formula = (for_all "x" (pApp "p" [x]) .&. (pApp "q" [x]))+ , expected = [PrenexNormalForm (for_all "x'" ((pApp "p" [vt ("x'")]) .&. ((pApp "q" [vt ("x")]))))]+ }+ , doTest $+ TestFormula+ { name = "skolemize2"+ , formula = exists "x" (for_all "y" (pApp "loves" [x, y]))+ , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x" 1) [],y])]+ }+ , doTest $+ TestFormula+ { name = "skolemize3"+ , formula = for_all "y" (exists "x" (pApp "loves" [x, y]))+ , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem "x" 1) [y],y])]+ }+ , doTest $+ 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" 1) [],+ vt ("y"),+ vt ("z"),+ fApp (toSkolem "u" 1) [vt ("y"),vt ("z")],+ vt ("v"),+ fApp (toSkolem "w" 1) [vt ("v"), vt ("y"),vt ("z")]]) ]+ }+ , doTest $+ 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")])]]) ]+ }+ , doTest $+ TestFormula+ { formula = n p0 .|. q0 .&. p0 .|. r0 .&. n q0 .&. n r0+ , name = "chang 7.2.1a - unsat"+ , expected = [ SatSolverSat False ] }+ , doTest $+ TestFormula+ { formula = p0 .|. q0 .|. r0 .&. n p0 .&. n q0 .&. n r0 .|. s0 .&. n s0+ , name = "chang 7.2.1b - unsat"+ , expected = [ SatSolverSat False ] }+ , doTest $+ 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" 1) [x,x,y,z],y]+ sk2 = f [fApp (toSkolem "x" 1) [x,x,y,z],x] in+ doTest $+ 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" :: SkTerm+ y = vt "y" :: SkTerm+ x' = vt "x" :: C.CTerm V Function+ y' = vt "y" :: C.CTerm V Function in+ doTest $+ TestFormula+ { name = "convert to Chiou 1"+ , formula = exists "x" (x .=. y)+ , expected = [ConvertToChiou (exists "x" (x' .=. y') :: C.Sentence V Predicate Function)]+ }+ , let s = pApp "s"+ s' = pApp "s"+ x' = vt "x"+ y' = vt "y" in+ doTest $+ 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+ doTest $+ 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+ doTest $+ 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" 1) [vt ("y")]]))],+ [(pApp ("wise") [vt ("y")]),+ ((.~.) (pApp ("wise") [fApp (toSkolem "x" 1) [vt ("y")]]))]])]+ }+ , doTest $+ 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"]))]] -}+ ]+ }+ , doTest $+ 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"])]])]+ }+ , doTest $+ 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"]))]])]+ }+ , doTest $+ 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"])]])]+ }+ , doTest $+ TestFormula+ { name = "cnf test 6"+ , formula = (exists "x" (p0 .=>. pApp "f" [x]))+ , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [])),(pApp "f" [fApp (toSkolem "x" 1) []])]])]+ }+ , let p = pApp "p" []+ f' = pApp "f" [x]+ f = pApp "f" [fApp (toSkolem "x" 1) []] in+ doTest $+ 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,Set.fromList [((.~.) (pApp ("p") [])),(pApp ("f") [fApp (toSkolem "x" 1) []])]),+ (False,Set.fromList [((.~.) (pApp ("f") [fApp (toSkolem "x" 1) []])),(pApp ("p") [])])]+ , ClauseNormalForm (toSS [[(f), ((.~.) p)], [p, ((.~.) f)]])]+ }+ , doTest $+ 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" 1) [vt "z"]])),(pApp "f" [vt "x",vt "z"])],+ [((.~.) (pApp "f" [vt "x",fApp (toSkolem "y" 1) [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" 1) [vt "z"]])]])]+ }+ , let f = pApp "f"+ q = pApp "q"+ (x, y, z) = (vt "x" :: SkTerm, vt "y" :: SkTerm, vt "z" :: SkTerm) in+ doTest $+ 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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [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" 1) [vt ("x"),vt ("y")]) (vt ("x"))),+ (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("y"))),+ (pApp2 ("q") (vt ("x")) (vt ("y")))],+ [(pApp2 ("q") (vt ("x")) (vt ("y"))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("x")))),+ ((.~.) (pApp2 ("f") (fApp (toSkolem "z" 1) [vt ("x"),vt ("y")]) (vt ("y"))))]])+ ]+ }+ , doTest $+ TestFormula+ { name = "cnf test 10"+ , formula = (for_all "x" (exists "y" ((for_all "x" (exists "z" (q [y, x, z]) .=>. r [y]) .=>. p [x, y]))))+ , expected = [ClauseNormalForm+ (toSS+ [[(pApp ("p") [vt ("x"),fApp (toSkolem "y" 1) [vt ("x")]]),+ (pApp ("q") [fApp (toSkolem "y" 1) [vt "x"],fApp (toSkolem "x'" 1) [vt "x"],fApp (toSkolem "z" 1) [vt "x"]])],+ [(pApp ("p") [vt ("x"),fApp (toSkolem "y" 1) [vt ("x")]]),+ ((.~.) (pApp ("r") [fApp (toSkolem "y" 1) [vt "x"]]))]])+ ]+ }+ , doTest $+ 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" 1) [vt "x",vt "z"]]))],+ [((.~.) (pApp "p" [vt "x",vt "z"])),(pApp "r" [fApp (toSkolem "y" 1) [vt "x",vt "z"],vt "z"])]])]+ }+ , doTest $+ 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 (f :: Formula) = for_all "x" ( x .=. x) .=>. for_all "x" (exists "y" ((x .=. y))) in+ doTest $+ TestFormula+ { name = "cnf test 13 " ++ prettyShow f+ , formula = f+ -- [[x = sKy[x], ¬sKx[] = sKx[]]]+ , expected = [ClauseNormalForm (toSS [[x .=. fApp (toSkolem "y" 1) [x], (.~.) (fApp (toSkolem "x" 1) [] .=. fApp (toSkolem "x" 1) [])]])]+ }+ , let p = pApp "p" [] in+ doTest $+ TestFormula+ { name = "psimplify 50"+ , formula = true .=>. (p .<=>. (p .<=>. false))+ , expected = [ SimplifiedForm (p .<=>. (.~.) p) ] }+ , doTest $+ TestFormula+ { name = "psimplify 51"+ , formula = (((pApp "x" [] .=>. pApp "y" []) .=>. true) .|. false)+ , expected = [ SimplifiedForm true ] }+ , let q = pApp "q" [] in+ doTest $+ 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" [])) ] }+ , doTest $+ 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"]))))))))))) ] }+ , doTest $+ 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" :: SkTerm, vt "y" :: SkTerm, vt "u" :: SkTerm, vt "v" :: SkTerm)+ fv = fApp (toSkolem "v" 1) [u,x]+ fy = fApp (toSkolem "y" 1) [x] in+ doTest $+ 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" :: SkTerm, vt "y" :: SkTerm, vt "z" :: SkTerm) in+ doTest $+ 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" 1) []) .|. (((.~.) (p z)) .|. ((.~.) (q z))))) ] }+ ]++animalKB :: (String, [TestFormula Formula SkAtom V])+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" 1) []])],[(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x" 1) []])]])]+ -- owns(jack,sK0)+ -- dog (SK0)+ }+ , TestFormula+ { formula = for_all "x" ((exists "y" (dog [y] .&. (owns [x, y]))) .=>. (animalLover [x])) -- [[Neg 1,Neg 2,Pos 3]]+ , name = "dog owners are animal lovers"+ , expected = [ PrenexNormalForm (for_all "x" (for_all "y" ((((.~.) (pApp "Dog" [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 :: [Test]+animalConjectures =+ let kills = pApp "Kills"+ jack = fApp "Jack" []+ tuna = fApp "Tuna" []+ curiosity = fApp "Curiosity" [] in++ map (doTest . 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 "x'"+ ((((pApp ("Dog") [vt ("x'")]) .&.+ ((pApp ("Owns") [fApp ("Jack") [],vt ("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 ("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" 1) []])],+ [(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),+ (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])],+ [(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x" 1) []])],+ [((.~.) (pApp ("Animal") [vt ("y")])),+ ((.~.) (pApp ("AnimalLover") [vt ("x")])),+ ((.~.) (pApp ("Kills") [vt ("x"),vt ("y")]))],+ [((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]))]])+ , ChiouKB1+ (Proof+ Invalid+ (Set.fromList+ [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])]),+ makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem "x" 1) []])]),+ makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),+ makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x" 1) []])]),+ 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" 1) []])],+ [(pApp "Owns" [fApp ("Jack") [],fApp (toSkolem "x" 1) []])],+ [((.~.) (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 :: forall t formula atom predicate v term.+ (atom ~ AtomOf formula, v ~ VarOf formula, term ~ TermOf atom, predicate ~ PredOf atom,+ Ord formula, IsString t,+ IsQuantified formula,+ HasApply atom,+ IsTerm term) =>+ (t, [TestFormula formula atom v])+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 "x'"])),(pApp "Mortal" [vt "x'"])],+ [((.~.) (pApp "Socrates" [vt "x'"])),(pApp "Human" [vt "x'"])],+ [(pApp "Socrates" [fApp (toSkolem "x" 1) [vt "x'",vt "x'"]])],+ [((.~.) (pApp "Mortal" [fApp (toSkolem "x" 1) [vt "x'",vt "x'"]]))]]+ , 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" 1) [x,y]])), (pApp "Human" [fApp (toSkolem "x" 1) [x,y]])],+ [(pApp "Socrates" [fApp (toSkolem "x" 1) [x,y]])], [((.~.) (pApp "Mortal" [fApp (toSkolem "x" 1) [x,y]]))]]+ , ClauseNormalForm [[((.~.) (pApp "Human" [vt "x'"])), (pApp "Mortal" [vt "x'"])],+ [((.~.) (pApp "Socrates" [vt "x'"])), (pApp "Human" [vt "x'"])],+ [((.~.) (pApp "Socrates" [vt "x"])), (pApp "Mortal" [vt "x"])]] ]+ }+ ]+-}++chang43KB :: (String, [TestFormula Formula SkAtom V])+chang43KB =+ let e = fApp "e" []+ (x, y, z, u, v, w) = (vt "x" :: SkTerm, vt "y" :: SkTerm, vt "z" :: SkTerm, vt "u" :: SkTerm, vt "v" :: SkTerm, vt "w" :: SkTerm) 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 :: Test+chang43Conjecture =+ let e = (fApp "e" [])+ (x, u, v, w) = (vt "x" :: SkTerm, vt "u" :: SkTerm, vt "v" :: SkTerm, vt "w" :: SkTerm) in+ doTest . 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 "z'"+ (exists "x'"+ (exists "u'"+ (exists "v'"+ (exists "w'"+ (((pApp ("P") [vt ("x"),vt ("y"),vt ("z'")]) .&.+ ((((((((.~.) (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") [vt ("u'"),vt ("v'"),vt ("w'")]) .&.+ (((.~.) (pApp ("P") [vt ("v'"),vt ("u'"),vt ("w'")])))))))))))))))))))+ , SkolemNormalForm+ (((pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z" 1) [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" 1) [],fApp (toSkolem "x" 1) [],fApp ("e") []]) .&.+ (((pApp ("P") [fApp (toSkolem "u" 1) [],fApp (toSkolem "v" 1) [],fApp (toSkolem "w" 1) []]) .&.+ (((.~.) (pApp ("P") [fApp (toSkolem "v" 1) [],fApp (toSkolem "u" 1) [],fApp (toSkolem "w" 1) []]))))))))+ , SkolemNumbers (Set.fromList [toSkolem "u" 1,toSkolem "v" 1,toSkolem "w" 1,toSkolem "x" 1,toSkolem "z" 1])+ -- From our algorithm++ , ClauseNormalForm+ (toSS+ [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z" 1) [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" 1) [],fApp (toSkolem "x" 1) [],fApp ("e") []])],+ [(pApp ("P") [fApp (toSkolem "u" 1) [],fApp (toSkolem "v" 1) [],fApp (toSkolem "w" 1) []])],+ [((.~.) (pApp ("P") [fApp (toSkolem "v" 1) [],fApp (toSkolem "u" 1) [],fApp (toSkolem "w" 1) []]))]])++ -- From the book+{-+ , let (a, b, c) =+ (fApp (toSkolem "x" 1) [vt ("x"),vt ("y"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u"),vt ("v"),vt ("w"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u'"),vt ("v'"),vt ("w'"),vt ("x''"),vt ("x''"),vt ("x''"),vt ("x''")],+ fApp (toSkolem "x" 1) [vt ("x"),vt ("y"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u"),vt ("v"),vt ("w"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u'"),vt ("v'"),vt ("w'"),vt ("x''"),vt ("x''"),vt ("x''"),vt ("x''")],+ fApp (toSkolem "x" 1) [vt ("x"),vt ("y"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u"),vt ("v"),vt ("w"),vt ("x'"),vt ("y'"),vt ("z'"),vt ("u'"),vt ("v'"),vt ("w'"),vt ("x''"),vt ("x''"),vt ("x''"),vt ("x''")]) in+ ClauseNormalForm+ [[(pApp "P" [vt "x",vt "y",fApp (toSkolem "x" 1) [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 :: Test+chang43ConjectureRenamed =+ let e = fApp "e" []+ (x, y, z, u, v, w) = (vt "x" :: SkTerm, vt "y" :: SkTerm, vt "z" :: SkTerm, vt "u" :: SkTerm, vt "v" :: SkTerm, vt "w" :: SkTerm)+ (u2, v2, w2, x2, y2, z2, u3, v3, w3, x3, y3, z3, x4, x5, x6, x7, x8) =+ (vt "u'" :: SkTerm, vt "v'" :: SkTerm, vt "w'" :: SkTerm, vt "x'" :: SkTerm, vt "y'" :: SkTerm, vt "z'" :: SkTerm, vt "u3" :: SkTerm, vt "v3" :: SkTerm, vt "w3" :: SkTerm, vt "x3" :: SkTerm, vt "y3" :: SkTerm, vt "z3" :: SkTerm, vt "x4" :: SkTerm, vt "x5" :: SkTerm, vt "x6" :: SkTerm, vt "x7" :: SkTerm, vt "x8" :: SkTerm) in+ doTest $+ TestFormula { name = "chang 43 renamed"+ , formula = (.~.) ((for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z])) .&.+ for_all' ["x'", "y'", "z'", "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", "u'", "v'", "w'"] (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' ["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' ["x3","y3","z3","u'","v'","w'"] ((((pApp "P" [vt "x3",vt "y3",vt "u'"]) .&.+ ((pApp "P" [vt "y3",vt "z3",vt "v'"]))) .&.+ ((pApp "P" [vt "x3",vt "v'",vt "w'"]))) .=>.+ ((pApp "P" [vt "u'",vt "z3",vt "w'"])))))) .&.+ ((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" 1) []+ b = fApp (toSkolem "v3" 1) []+ c = fApp (toSkolem "w3" 1) [] in+ ClauseNormalForm+ (toSS+ [[(pApp ("P") [vt ("x"),vt ("y"),fApp (toSkolem "z" 1) [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 "x8" 1) [],fApp (toSkolem "x8" 1) [],fApp ("e") []])],+ [(pApp ("P") [a,b,c])],+ [((.~.) (pApp ("P") [b,a,c]))]])+ ]+ }++withKB :: forall formula atom term v.+ (formula ~ Formula, atom ~ SkAtom, v ~ V,+ term ~ TermOf atom,+ IsQuantified formula, HasEquate atom, IsTerm term) =>+ (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.+ (formula ~ Formula, atom ~ SkAtom, v ~ V, term ~ TermOf atom,+ IsQuantified formula, HasEquate atom, IsTerm term) =>+ (String, [TestFormula formula atom v]) -> (String, [formula])+kbKnowledge kb = (fst (kb :: (String, [TestFormula formula atom v])), map formula (snd kb))++proofs :: [TestProof Formula SkAtom SkTerm 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 (Set.fromList+ [WithId {wiItem = INF (Set.fromList []) (Set.fromList [(pApp "Dog" [fApp (toSkolem "x" 1) []])]), wiIdent = 1},+ WithId {wiItem = INF (Set.fromList []) (Set.fromList [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x" 1) []])]), wiIdent = 1},+ WithId {wiItem = INF (Set.fromList [(pApp "Dog" [vt "y"]),(pApp "Owns" [vt "x",vt "y"])]) (Set.fromList [(pApp "AnimalLover" [vt "x"])]), wiIdent = 2},+ WithId {wiItem = INF (Set.fromList [(pApp "Animal" [vt "y"]),(pApp "AnimalLover" [vt "x"]),(pApp "Kills" [vt "x",vt "y"])]) (Set.fromList []), wiIdent = 3},+ WithId {wiItem = INF (Set.fromList []) (Set.fromList [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])]), wiIdent = 4},+ WithId {wiItem = INF (Set.fromList []) (Set.fromList [(pApp "Cat" [fApp "Tuna" []])]), wiIdent = 5},+ WithId {wiItem = INF (Set.fromList [(pApp "Cat" [vt "x"])]) (Set.fromList [(pApp "Animal" [vt "x"])]), wiIdent = 6}])+ , ChiouResult (False,+ (Set.fromList+ [(inf' [(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])] [],Map.fromList []),+ (inf' [] [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])],Map.fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "AnimalLover" [fApp "Curiosity" []])] [],Map.fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],Map.fromList []),+ (inf' [(pApp "AnimalLover" [fApp "Curiosity" []]),(pApp "Cat" [fApp "Tuna" []])] [],Map.fromList []),+ (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x" 1) []])] [],Map.fromList []),+ (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],Map.fromList []),+ (inf' [(pApp "AnimalLover" [fApp "Curiosity" []])] [],Map.fromList []),+ (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x" 1) []])] [],Map.fromList []),+ (inf' [(pApp "Dog" [vt "y"]),(pApp "Owns" [fApp "Curiosity" [],vt "y"])] [],Map.fromList []),+ (inf' [(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem "x" 1) []])] [],Map.fromList [])]))+ ]+ }+ , TestProof+ { proofName = "prove curiosity kills tuna"+ , proofKnowledge = kbKnowledge animalKB+ , conjecture = kills [curiosity, tuna]+ , proofExpected =+ [ ChiouKB (Set.fromList+ [WithId {wiItem = inf' [] [(pApp "Dog" [fApp (toSkolem "x" 1) []])], wiIdent = 1},+ WithId {wiItem = inf' [] [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem "x" 1) []])], 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,+ Set.fromList+ [(makeINF' ([]) ([]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),Map.fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x" 1) []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x" 1) []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem "x" 1) []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem "x" 1) []])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Dog") [vt ("y")]),(pApp ("Owns") [fApp ("Jack") [],vt ("y")])]) ([]),Map.fromList []),+ (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),Map.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 (Set.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,+ Set.fromList+ [(makeINF' ([]) ([]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([(pApp ("Mortal") [fApp (toSkolem "x" 1) []])]) ([]),Map.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 (Set.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+ ,(Set.fromList [(inf' [(pApp "Socrates" [vt "x"])] [(pApp "Mortal" [vt "x"])],Map.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 (Set.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,+ Set.fromList [(makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem "x" 1) []])]),Map.fromList []),+ (makeINF' ([(pApp ("Socrates") [vt ("x")])]) ([(pApp ("Mortal") [vt ("x")])]),Map.fromList [("x",vt ("x"))])])+ ]+ }+ ]++inf' :: (IsLiteral lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit+inf' = makeINF'++toLL :: Set (Set a) -> [[a]]+toLL = map Set.toList . Set.toList+toSS :: Ord a => [[a]] -> Set (Set a)+toSS = Set.fromList . map Set.fromList
+ Tests/Harrison/Common.hs view
@@ -0,0 +1,10 @@+{-# LANGUAGE FlexibleInstances, StandaloneDeriving #-}+module 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)++
+ Tests/Harrison/Equal.hs view
@@ -0,0 +1,251 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeSynonymInstances #-}+{-# OPTIONS_GHC -Wall #-}+module Harrison.Equal where++-- =========================================================================+-- First order logic with equality.+--+-- Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)+-- =========================================================================++import Common (render)+import Control.Applicative.Error (Failing(..))+import Data.List as List+import Data.Map as Map+import Data.Set as Set+import Data.String (IsString(fromString))+import Equal (equalitize, function_congruence)+import FOL ((.=.), (∃), (∀), IsTerm(..), pApp, Predicate, V)+import Formulas (IsCombinable(..), (∧), (⇒))+import Meson (meson)+import Prelude hiding ((*))+import Skolem (HasSkolem(..), MyTerm, MyFormula, runSkolem)+import Tableaux (Depth(Depth))+import Test.HUnit++-- type TF = TestFormula (Formula FOL) FOL MyTerm String String Function+-- type TFE = TestFormulaEq (MyFormula) FOLEQ MyTerm String String Function++tests :: Test+tests = TestLabel "Data.Logic.Tests.Harrison.Equal" $ TestList [test01, test02, test03, test04]++-- ------------------------------------------------------------------------- +-- Example. +-- ------------------------------------------------------------------------- ++test01 :: Test+test01 = TestCase $ assertEqual "function_congruence" expected input+ where input = List.map function_congruence [(fromString "f", 3 :: Int), (fromString "+",2)]+ expected :: [Set.Set (MyFormula)]+ 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+test label expected input = TestLabel label $ TestCase $ assertEqual label expected input++test02 :: Test+test02 = TestCase $ assertEqual "equalitize 1 (p. 241)" (expected, expectedProof) input+ where input = (render ewd, runSkolem (meson (Just (Depth 10)) ewd))+ ewd = equalitize fm :: MyFormula+ fm :: MyFormula+ 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) [] :: MyTerm)],0,1),1),+ Success ((Map.fromList [("_0",fApp (Skolem 2) [] :: MyTerm)],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),Depth 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 -> [MyTerm] -> MyFormula+ pApp' s ts = pApp (fromString s :: Predicate) ts+ --vt' :: String -> MyTerm+ --vt' s = vt (fromString s)++-- ------------------------------------------------------------------------- +-- Wishnu Prasetya's example (even nicer with an "exists unique" primitive). +-- ------------------------------------------------------------------------- ++wishnu :: MyFormula+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+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 (Depth 16)) wishnu))+ x = vt "x" :: MyTerm+ 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 :: MyFormula+ 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 ["Not sure what we git here if this finishes"]]+{-+ Set.fromList [Success ((Map.fromList [("_0",vt "_1")],0,2 :: Map.Map String MyTerm),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+test04 = TestCase $ assertEqual "equalitize 3 (p. 248)" (render expected, expectedProof) input+ where+ input = (render (equalitize fm), runSkolem (meson (Just (Depth 20)) . equalitize $ fm))+ fm :: MyFormula+ 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" :: MyTerm+ y' = vt "y" :: MyTerm+ z' = vt "z" :: MyTerm+ (*) = fApp (fromString "*")+ i = fApp (fromString "i")+ one = fApp (fromString "1") []+ expected :: MyFormula+ 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 V MyTerm, Int, Int), Depth))+ 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),Depth 13)]+ vt' = vt . fromString
+ Tests/Harrison/FOL.hs view
@@ -0,0 +1,221 @@+{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes,+ ScopedTypeVariables, TypeFamilies, TypeSynonymInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}+module Harrison.FOL+ ( tests1+ , tests2+ , example1+ , example2+ , example3+ , example4+ ) where++import Control.Applicative.Error (Failing(..))+import Control.Monad (filterM)+import qualified Data.Map as Map+import qualified Data.Set as Set+import FOL (for_all, exists, Predicate(Equals), MyFormula1,+ HasApplyAndEquate(..), (.=.), IsQuantified(..), IsTerm(vt, fApp, foldTerm), IsVariable(..), pApp, Quant(..))+import Formulas ((.~.), false, IsCombinable(..), BinOp(..))+import Lib ((|->))+import Prelude hiding (pred)+import Skolem (MyFormula, MyTerm, Function)+import Test.HUnit++tests1 :: Test+tests1 = TestLabel "Data.Logic.Tests.Harrison.FOL" $+ TestList [test01, test02, test03, test04, test05,+ test06, test07, test08, test09]+tests2 :: Test+tests2 = TestLabel "Data.Logic.Tests.Harrison.FOL" $+ TestList [{-test10, test11, test12-}]++-- ------------------------------------------------------------------------- +-- Semantics, implemented of course for finite domains only. +-- ------------------------------------------------------------------------- ++termval :: (IsTerm 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.+ (IsQuantified formula atom v, HasApplyAndEquate atom p term, IsTerm 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 =+ foldQuantified qu co ne tf at fm+ where+ qu op x p = mapM (\ a -> holds m ((|->) x a v) p) domain >>= return . (asPred op) (== True)+ asPred (:?:) = any+ asPred (:!:) = all+ ne p = holds m v p >>= return . not+ co p (:|:) q = (||) <$> (holds m v p) <*> (holds m v q)+ co p (:&:) q = (&&) <$> (holds m v p) <*> (holds m v q)+ co p (:=>:) q = (||) <$> (not <$> (holds m v p)) <*> (holds m v q)+ co p (:<=>:) q = (==) <$> (holds m v p) <*> (holds m v q)+ tf x = Success x+ at :: atom -> Failing Bool+ at = foldEquate (\ t1 t2 -> return $ termval m v t1 == termval m v t2) (\ r args -> mapM (termval m v) args >>= return . pred r)+-- | This becomes a method in FirstOrderFormulaEq, so it is not exported here.+-- (.=.) :: MyTerm -> MyTerm -> Formula FOL+-- a .=. b = Atom (R "=" [a, b])++-- -------------------------------------------------------------------------+-- Example. +-- -------------------------------------------------------------------------++{-+instance HasFixity (Formula FOL) where+ fixity = error "FIXME"+-}++example1 :: MyTerm+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 :: MyFormula1+example2 = pApp "<" [fApp "+" [vt "x", vt "y"], vt "z"]+-- example2 = Atom (R "<" [Fn "+" [Var "x", Var "y"], Var "z"])++-- ------------------------------------------------------------------------- +-- Example. +-- ------------------------------------------------------------------------- ++example3 :: MyFormula1+example3 = (for_all "x" (pApp "<" [vt "x", fApp "2" []] .=>.+ pApp "<=" [fApp "*" [fApp "2" [], vt "x"], fApp "3" []])) .|. false+example4 :: MyTerm+example4 = fApp "*" [fApp "2" [], vt "x"]++-- ------------------------------------------------------------------------- +-- Examples of particular interpretations. +-- ------------------------------------------------------------------------- ++boolInterp :: ([Bool], Function -> [Bool] -> Bool, Predicate -> [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+ (Equals, [x, y]) -> x == y+ _ -> error "uninterpreted predicate"++modInterp :: Integer+ -> ([Integer],+ Function -> [Integer] -> Integer,+ Predicate -> [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 :: Predicate -> [Integer] -> Bool+ pred p args =+ case (p,args) of+ (Equals,[x, y]) -> x == y+ _ -> error "uninterpreted predicate"++test01 :: Test+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" []) :: MyFormula)+ expected = Success True+test02 :: Test+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" [] :: MyTerm) .|. vt "x" .=. (fApp "1" [] :: MyTerm)) :: MyFormula)+ expected = Success True+test03 :: Test+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" []) :: MyFormula)+ expected = Success False++test04 :: Test+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" [])) :: MyFormula+ expected = Success [1,2,3,5,7,11,13,17,19,23,29,31,37,41,43]++test05 :: Test+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" [] :: MyFormula)+ expected = Success True+test06 :: Test+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" []) :: MyFormula)+ expected = Success False++-- ------------------------------------------------------------------------- +-- Variant function and examples. +-- ------------------------------------------------------------------------- ++test07 :: Test+test07 = TestCase $ assertEqual "variant 1 (p. 133)" expected input+ where input = variant "x" (Set.fromList ["y", "z"]) :: String+ expected = "x"+test08 :: Test+test08 = TestCase $ assertEqual "variant 2 (p. 133)" expected input+ where input = variant "x" (Set.fromList ["x", "y"]) :: String+ expected = "x'"+test09 :: Test+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" []+-}
+ Tests/Harrison/Main.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeSynonymInstances #-}+module Harrison.Main (tests) where++import qualified Harrison.Equal as Equal+import qualified Harrison.FOL as FOL+import qualified Harrison.Meson as Meson+import qualified Harrison.Prop as Prop+import qualified Harrison.Resolution as Resolution+import qualified Harrison.Skolem as Skolem+import qualified Harrison.Unif as Unif+import Test.HUnit++--instance Show MyFormula1 where+-- show = show . pPrint++-- main = runTestTT tests++tests :: Test+tests =+ TestList+ [ Prop.tests+ , FOL.tests1+ , FOL.tests2+ , Unif.tests+ , Skolem.tests+ , Resolution.tests+ , Equal.tests+ , Meson.tests+ ]
+ Tests/Harrison/Meson.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}+{-# OPTIONS_GHC -Wall #-}+module Harrison.Meson where++import Control.Applicative.Error (Failing(..))+import qualified Data.Map as Map+import qualified Data.Set as Set+import FOL (pApp)+import Formulas ((.&.), (.=>.), (.|.))+import FOL (exists, for_all)+import Formulas ((.~.))+import Skolem (HasSkolem(..))+import FOL (IsTerm(vt, fApp))+import FOL (generalize)+import Prop (list_conj)+import Meson(meson)+import Skolem (MyFormula, simpdnf')+import Skolem (runSkolem, askolemize)+import Data.String (IsString(fromString))+import Prelude hiding (negate)+import Test.HUnit (Test(TestCase, TestLabel, TestList), assertEqual)+import Tableaux (Depth(Depth))++import Common (render)+import Harrison.Resolution (dpExampleFm)++tests :: Test+tests = TestLabel "Data.Logic.Tests.Harrison.Meson" $+ TestList [test01, test02]++-- ------------------------------------------------------------------------- +-- Example. +-- ------------------------------------------------------------------------- ++test01 :: Test+test01 = TestLabel "Data.Logic.Tests.Harrison.Meson" $ TestCase $ assertEqual "meson dp example (p. 220)" expected input+ where input = runSkolem (meson (Just (Depth 10)) (dpExampleFm :: MyFormula))+ 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),Depth 8)+ )+ vt' = vt . fromString++test02 :: Test+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]))))))) :: MyFormula))+ (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))) :: MyFormula))),+ 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))) :: MyFormula)))),+ 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 MyFormula)))]+ 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)))>>+-}
+ Tests/Harrison/Prop.hs view
@@ -0,0 +1,404 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies #-}+{-# OPTIONS_GHC -Wall -Wwarn #-}+module Harrison.Prop+ ( tests+ ) where++import Data.Set as Set (filter, fromList, Set)+import Formulas (IsCombinable(..), (∨), (∧), true, false, atomic, (.~.), (¬))+import Lib ((|=>))+import Prelude hiding (negate)+import Prop (atoms, cnf', dnf, dual, eval, Literal, Marked, nnf, PFormula(Atom, Not, Imp, Iff, Or, And), Prop(..),+ psimplify, psubst, purednf, rawdnf, tautology, trivial, truthTable, TruthTable(TruthTable))+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 :: [PFormula 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 (const False), flag)) pairs)+ pairs :: [(PFormula 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 =+ (TruthTable+ [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)+ (TruthTable+ [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 = (TruthTable+ [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)),+ (TruthTable+ [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 :: PFormula 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 id $ (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))+ expected :: Set (Set (Marked Literal (PFormula Prop)))+ expected = Set.fromList [Set.fromList [p, (.~.) p],+ Set.fromList [p, (.~.) r],+ Set.fromList [q, r, (.~.) p],+ Set.fromList [q, r, (.~.) r]]+ p = atomic (P "p")+ q = atomic (P "q")+ r = atomic (P "r")++-- ------------------------------------------------------------------------- +-- Example. +-- ------------------------------------------------------------------------- ++test33 :: Test+test33 = TestCase $ assertEqual "trivial" expected input+ where input = Set.filter (not . trivial) (purednf id fm)+ expected :: Set (Set (Marked Literal (PFormula Prop)))+ expected = Set.fromList [Set.fromList [p, (.~.) r],+ Set.fromList [q, r, (.~.) p]]+ fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))+ p = atomic (P "p")+ q = atomic (P "q")+ r = atomic (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")
+ Tests/Harrison/Resolution.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wall #-}+module Harrison.Resolution where++import FOL (pApp)+import Control.Applicative.Error (Failing(..))+import Formulas (IsCombinable(..))+import Formulas ((.~.))+import FOL (IsTerm(vt, fApp))+import Skolem (simpcnf')+import Resolution (resolution1, resolution2, resolution3, presolution)+import Skolem (runSkolem)+import Skolem (MyFormula)+import FOL (exists, for_all)+import qualified Data.Set as Set+import Data.String (IsString(..))+import Prelude hiding (negate)+import Skolem (MyTerm, toSkolem)+import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)++tests :: Test+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+test01 = TestCase $ assertEqual "Barber's paradox (p. 181)" expected input+ where input = simpcnf' ((.~.)barb)+ barb :: MyFormula+ 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 (toSkolem "x")+ shaves = pApp (fromString "shaves") ++-- ------------------------------------------------------------------------- +-- Simple example that works well. +-- ------------------------------------------------------------------------- ++test02 :: Test+test02 = TestCase $ assertEqual "Davis-Putnam example" expected input+ where input = runSkolem (resolution1 (dpExampleFm :: MyFormula))+ expected = Set.singleton (Success True)++dpExampleFm :: MyFormula+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" :: MyTerm+ y = vt "y"+ z = vt "z"+ g = pApp "G" :: [MyTerm] -> MyFormula+ f = pApp "F"++-- ------------------------------------------------------------------------- +-- This is now a lot quicker. +-- ------------------------------------------------------------------------- ++test03 :: Test+test03 = TestCase $ assertEqual "Davis-Putnam example 2" expected input+ where input = runSkolem (resolution2 (dpExampleFm :: MyFormula))+ expected = Set.singleton (Success True)++-- ------------------------------------------------------------------------- +-- Example: the (in)famous Los problem. +-- ------------------------------------------------------------------------- ++test04 :: Test+test04 = TestCase $ assertEqual "Los problem (p. 198)" expected input+ where input = runSkolem (presolution losFm)+ expected = Set.fromList [Success True]++losFm :: MyFormula+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+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 :: MyFormula+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 :: MyFormula+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")
+ Tests/Harrison/Skolem.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}+{-# OPTIONS_GHC -Wall #-}+module Harrison.Skolem+ ( tests+ ) where++import FOL (exists, for_all, IsTerm(..), pApp)+import Formulas (IsCombinable(..), false, (.~.))+import Prop (PFormula)+import Skolem (MyAtom, MyFormula, nnf, pnf, runSkolem, simplify, skolemize, toSkolem)+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 []) :: MyFormula+ fm :: MyFormula+ 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 :: MyFormula+ 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 :: MyFormula+ 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) :: PFormula MyAtom+ fm :: MyFormula+ 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 (toSkolem "y") [vt "x"]])) .|.+ (pApp ({-Named -}"<") [fApp "*" [vt "x",vt "u"],fApp "*" [fApp (toSkolem "y") [vt "x"],fApp (toSkolem "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) :: PFormula MyAtom+ fm :: MyFormula+ 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 (toSkolem "y") []]) .|.+ (((.~.)(pApp p [vt "z"])) .|.+ ((.~.)(pApp q [vt "z"]))))
+ Tests/Harrison/Unif.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wall -Wwarn #-}+module Harrison.Unif+ ( tests+ ) where++import FOL (IsTerm(fApp, vt), tsubst)+import Lib (Failing(..), failing)+import Unif (fullunify)+import FOL (Term)+import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)+import FOL (FName)++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 :: [[(Term FName String, Term FName String)]]+ 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"])] ]
+ Tests/Logic.hs view
@@ -0,0 +1,636 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,+ ScopedTypeVariables, TypeFamilies, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall -Wwarn -fno-warn-name-shadowing -fno-warn-orphans #-}+module Logic (tests) where++import Common ({-instance Atom SkAtom SkTerm V-})+import Data.List as List (map)+import Data.Logic.ATP.Apply (applyPredicate, HasApply(TermOf, PredOf), pApp, Predicate)+import Data.Logic.ATP.Equate ((.=.), HasEquate(equate))+import Data.Logic.ATP.FOL (fv, subst, IsFirstOrder)+import Data.Logic.ATP.Formulas (atomic, IsFormula(AtomOf))+import Data.Logic.ATP.Lit ((.~.), convertLiteral, IsLiteral, LFormula)+import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint))+import Data.Logic.ATP.Prop ((⇒), IsPropositional(..), list_conj, list_disj, PFormula, simpcnf, TruthTable(..), TruthTable, truthTable)+import Data.Logic.ATP.Quantified ((∀), exists, for_all, IsQuantified(VarOf))+import Data.Logic.ATP.Skolem (HasSkolem(..), runSkolem, skolemize, pnf, simpcnf', Function)+import Data.Logic.ATP.Term (vt, IsTerm(FunOf), V(V), fApp)+import Data.Logic.Classes.Atom (Atom)+import Data.Logic.Instances.Test (Formula, SkAtom, SkTerm)+import Data.Logic.Satisfiable (theorem, inconsistant)+import Data.Map as Map (singleton)+import Data.Set.Extra as Set (Set, singleton, toList, empty, fromList, map {-, minView, fold-})+import Data.String (IsString(fromString))+import Test.HUnit+import qualified TextDisplay as TD++tests :: Test+tests = TestLabel "Test.Logic" $ TestList [precTests, normalTests, theoremTests]++{-+formCase :: (IsQuantified TFormula TAtom V, HasEquality TAtom Pr TTerm, Term TTerm V AtomicFunction) =>+ String -> TFormula -> TFormula -> Test+formCase s expected input = TestLabel s $ TestCase (assertEqual s expected input)+-}++-- instance IsAtom (Predicate Pr (PTerm V AtomicFunction))++precTests :: Test+precTests =+ TestList+ [ let label = "Logic - prec test 1" in+ TestLabel label (TestCase (assertEqual label+ ((a .&. b) .|. c)+ (a .&. b .|. c)))+ -- You can't apply .~. without parens:+ -- :type (.~. a) -> (FormulaPF -> t) -> t+ -- :type ((.~.) a) -> FormulaPF+ , let label = "Logic - prec test 2" in+ TestLabel label (TestCase (assertEqual label+ (((.~.) a) .&. b)+ ((.~.) a .&. b :: Formula)))+ -- 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.+ , let label = "Logic - prec test 3" in+ TestLabel label (TestCase (assertEqual label+ ((a .&. b) .&. c) -- infixl, with infixr we get (a .&. (b .&. c))+ (a .&. b .&. c :: Formula)))+ , let -- x = vt "x" :: SkTerm+ y = vt "y" :: SkTerm+ -- 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]) :: Formula+ input = (∀) "y" (pApp "g" [y]) ⇒ (pApp "f" [y]) :: Formula in+ let label = "Logic - prec test 4" in+ TestLabel label (TestCase (assertEqual label expected input))+ , TestCase (assertEqual "Logic - Find a free variable"+ (fv (for_all "x" (x .=. y) :: Formula))+ (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"+ (List.map sub+ [ for_all "x" (x .=. y) {- :: Formula String String -}+ , for_all "y" (x .=. y) {- :: Formula String String -} ])+ [ for_all "x" (x .=. z) :: Formula+ , for_all "y" (z .=. y) :: Formula ])+ ]+ where+ sub f = subst (Map.singleton (head . Set.toList . fv $ f) (vt "z")) f+ a = pApp ("a") []+ b = pApp ("b") []+ c = pApp ("c") []++x :: SkTerm+x = vt (fromString "x")+y :: SkTerm+y = vt (fromString "y")+z :: SkTerm+z = vt (fromString "z")++normalTests :: Test+normalTests =+ let s = pApp "S"+ h = pApp "H"+ m = pApp "M"+ x' = vt "x'" :: SkTerm+ for_all' x fm = for_all (fromString x) fm+ exists' x fm = exists (fromString x) fm+ in+ TestList+ [TestCase (assertEqual+ "nnf"+ (show (pPrint (for_all' "x" (exists' "x'" ((s[x'] .&. ((.~.)(h[x'])) .|. h[x'] .&. ((.~.)(m[x']))) .|. ((.~.)(s[x])) .|. m[x])) :: Formula)))+ -- <<forall x. exists x'. (S(x') /\ ~H(x') \/ H(x') /\ ~M(x')) \/ ~S(x) \/ M(x)>>+ -- ∀x. ∃x'. ((S(x') ∧ ¬H(x') ∨ H(x') ∧ ¬M(x')) ∨ ¬S(x) ∨ M(x))+ (show+ (pPrint+ (pnf (((for_all' "x" (s[x] .=>. h[x])) .&. (for_all "x" (h[x] .=>. m[x]))) .=>.+ (for_all "x" (s[x] .=>. m[x])) :: Formula) :: Formula))))]++-- |Here is an example of automatic conversion from a IsQuantified+-- instance to a IsPropositional 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 IsPropositional 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 Formula+ 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 :: Formula+ 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 :: Formula+ 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 :: Formula+ expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [],y])+ formula :: Formula+ formula = snf' (exists ["x"] (for_all ["y"] (pApp "loves" [x, y])))++skolemize3 :: Test+skolemize3 =+ myTest "Logic - skolemize3" expected formula+ where+ expected :: Formula+ expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [y],y])+ formula :: Formula+ formula = snf' (for_all ["y"] (exists ["x"] (pApp "loves" [x, y])))+-}+{-+inf1 :: Test+inf1 =+ myTest "Logic - inf1" expected formula+ where+ expected :: Formula+ 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 => -} Formula+ 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)+-}++equality1 :: Formula+equality1 = for_all "x" ( x .=. x) .=>. for_all "x" (exists "y" ((x .=. y))) :: Formula+equality1expected :: (Bool, (Set (Set (LFormula SkAtom)), TruthTable SkAtom))+equality1expected = (False,(fromList [fromList [(vt "x" .=. fApp (toSkolem "y" 1)[vt "x"]) :: LFormula SkAtom,+ ((.~.) (fApp (toSkolem "x" 1)[] .=. fApp (toSkolem "x" 1)[])) :: LFormula SkAtom]],+ TruthTable [equate (vt (V "x")) ((fApp (toSkolem (V "y") 1 :: Function)[vt (V "x")] :: SkTerm)),+ equate (fApp (toSkolem (V "x") 1)[]) (fApp (toSkolem (V "x") 1)[] :: SkTerm)]+ [([False,False],True),+ ([False,True],False),+ ([True,False],True),+ ([True,True],True)]))+{-+equality1expected = (False, (fromList [fromList [markLiteral (markPropositional ((vt "x" :: SkTerm) .=. fApp (toSkolem "y" 1)[vt (V "x")])),+ markLiteral (markPropositional ((.~.) ((fApp (toSkolem "x" 1)[] :: SkTerm) .=. (fApp (toSkolem "x" 1)[] :: SkTerm))))]],+ TruthTable ([{-(vt "x" :: SkTerm) .=. (fApp (toSkolem ("y" :: V) 1) [vt (V "x")] :: SkTerm),+ fApp (toSkolem "x" 1) [] .=. fApp (toSkolem "x" 1) []-}] :: [SkAtom])+ [([False,False],True),+ ([False,True],False),+ ([True,False],True),+ ([True,True],True)]))+-}+-- equality1expected = (False, (fromList [], TruthTable [] []))+{-+ concat ["({{x = sKy[x], ¬(sKx[] = sKx[])}},\n",+ " ([x = sKy[x], sKx[] = sKx[]],\n",+ " [([False, False], True), ([False, True], False),\n",+ " ([True, False], True), ([True, True], True)]))"]-}+equality2 :: Formula+equality2 = for_all "x" ( x .=. x .=>. for_all "x" ((.~.) (for_all "y" ((.~.) (x .=. y))))) -- convert existential+equality2expected :: (Bool, (Set (Set (LFormula SkAtom)), TruthTable SkAtom))+equality2expected = (False, (fromList [fromList [(vt (V "x'") .=. fApp (toSkolem (V "y") 1)[vt (V "x'")]) :: LFormula SkAtom,+ ((.~.) (vt (V "x") .=. vt (V "x"))) :: LFormula SkAtom]],+ TruthTable [equate (vt (V "x")) (vt (V "x")),+ equate (vt (V "x'")) (fApp (toSkolem (V "y") 1)[vt "x'"] :: SkTerm)]+ [([False, False], True),+ ([False, True], True),+ ([True, False], False),+ ([True, True], True)]))+{-+equality2expected = (False,+ concat ["({{x2 = sKy[x2], ¬x = x}},\n",+ " ([x = x, x2 = sKy[x2]],\n",+ " [([False, False], True), ([False, True], True),\n",+ " ([True, False], False), ([True, True], True)]))"])+-}+theoremTests :: Test+theoremTests =+ let s = pApp "S" :: [SkTerm] -> Formula+ h = pApp "H" :: [SkTerm] -> Formula+ m = pApp "M" :: [SkTerm] -> Formula+ socrates1 = (for_all "x" (s [x] .=>. h [x]) .&. for_all "x" (h [x] .=>. m [x])) .=>. for_all "x" (s [x] .=>. m [x]) :: Formula -- First two clauses grouped - compare to 5+ socrates2 = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x])) :: Formula -- shared binding for x+ socrates3 = (for_all "x" ((s [x] .=>. h [x]) .&. (h [x] .=>. m [x]))) .=>. (for_all "y" (s [y] .=>. m [y])) :: Formula -- 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]) :: Formula -- 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]) :: Formula -- 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+ [ let label = "Logic - equality1" in+ TestLabel label (TestCase (assertEqual' label+ equality1expected+ (theorem equality1, table' equality1)))+ , let label = "Logic - equality2" in+ TestLabel label (TestCase (assertEqual' label+ equality2expected+ (theorem equality2, table' equality2)))+ , let label = "Logic - theorem test 1" in+ TestLabel label (TestCase (assertEqual label+ (True,(Set.empty, (TruthTable []{-Just (CJ [])-} [([],True)])))+ (theorem socrates2, table' socrates2)))+ , let label = "Logic - theorem test 1a" in+ TestLabel label (TestCase (assertEqual' label+ (False,+ False,+ (fromList [fromList [atomic (applyPredicate "H" [fApp (toSkolem "x" 1) []]),+ atomic (applyPredicate "M" [vt "y"]),+ atomic (applyPredicate "S" [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate "S" [vt "y"]))],+ fromList [atomic (applyPredicate "M" [vt "y"]),+ atomic (applyPredicate "S" [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate "M" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "S" [vt "y"]))],+ fromList [atomic (applyPredicate "M" [vt "y"]),+ (.~.) (atomic (applyPredicate "H" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "M" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "S" [vt "y"]))]],+ (TruthTable+ [(applyPredicate "H" [fApp (toSkolem "x" 1) []]),+ (applyPredicate "M" [vt ("y")]),+ (applyPredicate "M" [fApp (toSkolem "x" 1) []]),+ (applyPredicate "S" [vt ("y")]),+ (applyPredicate "S" [fApp (toSkolem "x" 1) []])]+ [([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)])))++ (theorem socrates3, inconsistant socrates3,+ table' socrates3)))+ , let label = "socrates1 truth table" in+ TestLabel label (TestCase (assertEqual' label+ (let skx = fApp (toSkolem "x" 1) in+ (fromList [fromList [atomic (applyPredicate "H" [fApp (toSkolem "x" 1) []]),+ atomic (applyPredicate "M" [vt "x"]),+ atomic (applyPredicate "S" [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate "S" [vt "x"]))],+ fromList [atomic (applyPredicate "M" [vt "x"]),+ atomic (applyPredicate "S" [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate "M" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "S" [vt "x"]))],+ fromList [atomic (applyPredicate "M" [vt "x"]),+ (.~.) (atomic (applyPredicate "H" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "M" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "S" [vt "x"]))]],+ (TruthTable+ [(applyPredicate "H" [skx []]),+ (applyPredicate "M" [x]),+ (applyPredicate "M" [skx []]),+ (applyPredicate "S" [x]),+ (applyPredicate "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" 1)+ {- sky = fApp (toSkolem "y" 1) -} in+ let label = "Socrates formula skolemized" in+ TestLabel label (TestCase (assertEqual' label+ (((pApp "S" [skx []] .&. (.~.)(pApp "H" [skx []]) .|. pApp "H" [skx[]] .&. (.~.)(pApp "M" [skx []])) .|.+ ((.~.)(pApp "S" [x]) .|. pApp "M" [x])))+ (runSkolem (skolemize id socrates5) :: PFormula SkAtom)))++ , let skx = fApp (toSkolem "x" 1)+ sky = fApp (toSkolem "y" 1) in+ let label = "Socrates formula skolemized" in+ TestLabel label (TestCase (assertEqual' label+ ((pApp "S" [skx []] .&. (.~.)(pApp "H" [skx []]) .|. pApp "H" [sky[]] .&. (.~.)(pApp "M" [sky []])) .|.+ ((.~.)(pApp "S" [z]) .|. pApp "M" [z]))+ (runSkolem (skolemize id socrates6) :: PFormula SkAtom)))++ , let label = "Logic - socrates is not mortal" in+ TestLabel label (TestCase (assertEqual' label+ (False,+ False,+ (fromList [fromList [atomic (applyPredicate "H" [vt "x"]),+ (.~.) (atomic (applyPredicate "S" [vt "x"]))],+ fromList [atomic (applyPredicate "M" [vt "x"]),+ (.~.) (atomic (applyPredicate "H" [vt "x"]))],+ fromList [atomic (applyPredicate "S" [fApp "socrates" []])],+ fromList [(.~.) (atomic (applyPredicate "M" [vt "x"])),+ (.~.) (atomic (applyPredicate "S" [vt "x"]))]],+ (TruthTable+ [(applyPredicate ("H") [vt ("x")]),+ (applyPredicate ("M") [vt ("x")]),+ (applyPredicate ("S") [vt ("x")]),+ (applyPredicate ("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 ("S") [fApp ("socrates") []])],+ [(pApp ("H") [vt ("x")]),((.~.) (pApp ("S") [vt ("x")]))],+ [(pApp ("M") [vt ("x")]),((.~.) (pApp ("H") [vt ("x")]))],+ [((.~.) (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?+ (theorem socrates7, inconsistant socrates7, table' socrates7, simpcnf' socrates7 :: Set (Set Formula))))+ , let (formula :: Formula) =+ (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 [atomic (applyPredicate "L" [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate "F" [vt "x'"])),+ (.~.) (atomic (applyPredicate "L" [vt "x"]))],+ fromList [(.~.) (atomic (applyPredicate "F" [vt "x'"])),+ (.~.) (atomic (applyPredicate "F" [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate "L" [vt "x"]))]],+ (TruthTable+ [(applyPredicate ("F") [vt ("x'")]),+ (applyPredicate ("F") [fApp (toSkolem "x" 1) []]),+ (applyPredicate ("L") [vt ("x")]),+ (applyPredicate ("L") [fApp (toSkolem "x" 1) []])]+ [([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 let label = "Logic - gensler189" in+ TestLabel label (TestCase (assertEqual' label expected input))+ , let (formula :: Formula) =+ (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 [atomic (applyPredicate (p "L") [fApp (toSkolem "x" 1) []]),+ (.~.) (atomic (applyPredicate (p "F") [vt "z"])),+ (.~.) (atomic (applyPredicate (p "L") [vt "y"]))],+ fromList [(.~.) (atomic (applyPredicate (p "F") [vt "z"])),+ (.~.) (atomic (applyPredicate (p "F") [fApp (toSkolem "x" 1) []])),+ (.~.) (atomic (applyPredicate (p "L") [vt "y"]))]],+ (TruthTable+ [applyPredicate (p "F") [vt (V "z")],+ applyPredicate (p "F") [fApp (toSkolem (V "x") 1) []],+ applyPredicate (p "L") [vt (V "y")],+ applyPredicate (p "L") [fApp (toSkolem (V "x") 1) []]]+ [([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 let label = "Logic - gensler189 renamed" in+ TestLabel label (TestCase (assertEqual label expected input))+ ]++p :: String -> Predicate+p = fromString++toSS :: Ord a => [[a]] -> Set (Set a)+toSS = Set.fromList . List.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 Formula where+ textFrame x = [show 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.+ (IsQuantified formula atom v,+ IsPropositional formula atom,+ Atom atom term v,+ HasEquality atom p term,+ HasBoolean p, Eq p, Term term v f, IsLiteral formula atom v,+ Ord formula, Skolem f v, IsString v, Variable v, TD.Display formula) => -}++table :: forall formula atom p term v f.+ (atom ~ AtomOf formula, v ~ VarOf formula, v ~ SVarOf f, term ~ TermOf atom, p ~ PredOf atom, f ~ FunOf term,+ IsFirstOrder formula,+ IsPropositional formula,+ IsLiteral formula,+ HasSkolem f,+ Atom atom term v,+ IsTerm term,+ Ord formula, Pretty formula, Ord atom) =>+ formula -> (Set (Set (LFormula atom)), TruthTable (AtomOf formula))+table f =+ -- truthTable :: Ord a => PropForm a -> TruthTable a+ (cnf, truthTable cnf')+ where+ cnf' :: PFormula atom+ cnf' = list_conj (Set.map (list_disj . Set.map (convertLiteral id)) cnf)+ cnf :: Set (Set (LFormula atom))+ cnf = simpcnf id (runSkolem (skolemize id f) :: PFormula atom)+ -- fromSS = List.map Set.toList . Set.toList+ -- n f = (if negated f then (.~.) . atomic . (.~.) else atomic) $ f+ -- list_disj = setFoldr1 (.|.)+ -- list_conj = setFoldr1 (.&.)++table' :: Formula -> (Set (Set (LFormula SkAtom)), TruthTable SkAtom)+table' = table++{-+setFoldr1 :: (a -> a -> a) -> Set a -> a+setFoldr1 f s =+ case Set.minView s of+ Nothing -> error "setFoldr1"+ Just (x, s') -> Set.fold f x s'+-}
+ Tests/TPTP.hs view
@@ -0,0 +1,22 @@+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.7.1) unstable; urgency=low++ * Log entry to match cabal version.++ -- David Fox <dsf@seereason.com> Sun, 18 Sep 2016 08:06:40 -0700+ haskell-logic-classes (1.5.3) unstable; urgency=low * Make the Show instances output more general expressions
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name: logic-classes-Version: 1.7+Version: 1.7.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@@ -19,7 +19,7 @@ flag local-atp-haskell Manual: True- Default: True+ Default: False Library GHC-options: -Wall -O2@@ -65,4 +65,18 @@ GHC-Options: -Wall -O2 -fno-warn-orphans Hs-Source-Dirs: Tests Main-Is: Main.hs+ Other-modules: Chiou0+ Common+ Data+ Harrison.Common+ Harrison.Equal+ Harrison.FOL+ Harrison.Main+ Harrison.Meson+ Harrison.Prop+ Harrison.Resolution+ Harrison.Skolem+ Harrison.Unif+ Logic+ TPTP Build-Depends: applicative-extras, atp-haskell, base, containers, HUnit, logic-classes, mtl, pretty >= 1.1.2, PropLogic, safe, set-extra, syb