diff --git a/Data/Logic/Classes/Atom.hs b/Data/Logic/Classes/Atom.hs --- a/Data/Logic/Classes/Atom.hs +++ b/Data/Logic/Classes/Atom.hs @@ -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 diff --git a/Data/Logic/Types/FirstOrder.hs b/Data/Logic/Types/FirstOrder.hs --- a/Data/Logic/Types/FirstOrder.hs +++ b/Data/Logic/Types/FirstOrder.hs @@ -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) diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -6,5 +6,4 @@ import System.Directory (copyFile) main :: IO () -main = copyFile "debian/changelog" "changelog" >> - defaultMainWithHooks simpleUserHooks +main = defaultMainWithHooks simpleUserHooks diff --git a/Tests/Chiou0.hs b/Tests/Chiou0.hs new file mode 100644 --- /dev/null +++ b/Tests/Chiou0.hs @@ -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"]))] diff --git a/Tests/Common.hs b/Tests/Common.hs new file mode 100644 --- /dev/null +++ b/Tests/Common.hs @@ -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 diff --git a/Tests/Data.hs b/Tests/Data.hs new file mode 100644 --- /dev/null +++ b/Tests/Data.hs @@ -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 diff --git a/Tests/Harrison/Common.hs b/Tests/Harrison/Common.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Common.hs @@ -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) + + diff --git a/Tests/Harrison/Equal.hs b/Tests/Harrison/Equal.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Equal.hs @@ -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 diff --git a/Tests/Harrison/FOL.hs b/Tests/Harrison/FOL.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/FOL.hs @@ -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" [] +-} diff --git a/Tests/Harrison/Main.hs b/Tests/Harrison/Main.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Main.hs @@ -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 + ] diff --git a/Tests/Harrison/Meson.hs b/Tests/Harrison/Meson.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Meson.hs @@ -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]])))]])) +{- +[[<>]] +-} + (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]])))])) +{- +[<>] +-} + (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)) -> + <> +-} diff --git a/Tests/Harrison/Prop.hs b/Tests/Harrison/Prop.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Prop.hs @@ -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") diff --git a/Tests/Harrison/Resolution.hs b/Tests/Harrison/Resolution.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Resolution.hs @@ -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") diff --git a/Tests/Harrison/Skolem.hs b/Tests/Harrison/Skolem.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Skolem.hs @@ -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"])))) diff --git a/Tests/Harrison/Unif.hs b/Tests/Harrison/Unif.hs new file mode 100644 --- /dev/null +++ b/Tests/Harrison/Unif.hs @@ -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"])] ] diff --git a/Tests/Logic.hs b/Tests/Logic.hs new file mode 100644 --- /dev/null +++ b/Tests/Logic.hs @@ -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))) + -- <> + -- ∀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' +-} diff --git a/Tests/TPTP.hs b/Tests/TPTP.hs new file mode 100644 --- /dev/null +++ b/Tests/TPTP.hs @@ -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) diff --git a/changelog b/changelog --- a/changelog +++ b/changelog @@ -1,3 +1,9 @@ +haskell-logic-classes (1.7.1) unstable; urgency=low + + * Log entry to match cabal version. + + -- David Fox 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 diff --git a/logic-classes.cabal b/logic-classes.cabal --- a/logic-classes.cabal +++ b/logic-classes.cabal @@ -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