packages feed

logic-classes (empty) → 0.44

raw patch · 41 files changed

+5515/−0 lines, 41 filesdep +HUnitdep +PropLogicdep +basebuild-type:Customsetup-changed

Dependencies added: HUnit, PropLogic, base, containers, fgl, happstack-data, incremental-sat-solver, mtl, pretty, safecopy, set-extra, syb, syb-with-class, text

Files

+ Data/Logic.hs view
@@ -0,0 +1,47 @@+{-# OPTIONS -Wwarn #-}+module Data.Logic+    ( -- * Boolean Logic+      Negatable(..)+    , Boolean(fromBool)+    , Logic(..)+    -- * Propositional Logic+    , PropositionalFormula(..)+    , Combine(..)+    , BinOp(..)+    -- * FirstOrderLogic+    , Variable(..)+    , Arity(arity)+    , Pred(..)+    , pApp+    , Predicate(..)+    , Skolem(..)+    , Term(..)+    , FirstOrderFormula(..)+    -- * Normal Forms+    , Literal(..)+    , ClauseNormalFormula(..)+    , ImplicativeForm(..)+    -- * Knowledge Base and Theorem Proving+    , Proof(proofResult)+    , ProofResult(Proved, Invalid, Disproved)+    , tellKB+    , runProverT'+    , prettyProof+    ) where++import Data.Logic.Classes.Arity+import Data.Logic.Classes.Boolean+import Data.Logic.Classes.ClauseNormalForm+import Data.Logic.Classes.FirstOrder+import Data.Logic.Classes.Literal+import Data.Logic.Classes.Logic+import Data.Logic.Classes.Negatable+import Data.Logic.Classes.Pred+import Data.Logic.Classes.Propositional+import Data.Logic.Classes.Skolem+import Data.Logic.Classes.Term+import Data.Logic.Classes.Variable+import Data.Logic.KnowledgeBase+import Data.Logic.Normal.Implicative+import Data.Logic.Types.FirstOrder ()+import Data.Logic.Types.FirstOrderPublic ()
+ Data/Logic/Classes/Arity.hs view
@@ -0,0 +1,10 @@+module Data.Logic.Classes.Arity+    ( Arity(arity)+    ) where++-- |A class that characterizes how many arguments a predicate or+-- function takes.  Depending on the context, a result of Nothing may+-- mean that the arity is undetermined or unknown, or that any number+-- of arguments may be passed.+class Arity p where+    arity :: p -> Maybe Int
+ Data/Logic/Classes/Boolean.hs view
@@ -0,0 +1,8 @@+module Data.Logic.Classes.Boolean+    ( Boolean(fromBool)+    ) where++-- |Some types in the Logic class heirarchy need to have True and+-- False elements.+class Boolean p where+    fromBool :: Bool -> p
+ Data/Logic/Classes/ClauseNormalForm.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-}+module Data.Logic.Classes.ClauseNormalForm+    ( ClauseNormalFormula(clauses, makeCNF, satisfiable)+    ) where++import Control.Monad (MonadPlus)+import Data.Logic.Classes.Negatable+import Data.Set as S++-- |A class to represent formulas in CNF, which is the conjunction of+-- a set of disjuncted literals each which may or may not be negated.+class (Negatable lit, Eq lit, Ord lit) => ClauseNormalFormula cnf lit | cnf -> lit where+    clauses :: cnf -> S.Set (S.Set lit)+    makeCNF :: S.Set (S.Set lit) -> cnf+    satisfiable :: MonadPlus m => cnf -> m Bool
+ Data/Logic/Classes/FirstOrder.hs view
@@ -0,0 +1,350 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, FunctionalDependencies,+             MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, UndecidableInstances #-}+module Data.Logic.Classes.FirstOrder+    ( FirstOrderFormula(..)+    , Quant(..)+    , Predicate(..)+    , quant+    , (!), (?)+    , quant'+    , for_all'+    , exists'+    , freeVars+    , withUnivQuants+    , quantVars+    , allVars+    , univquant_free_vars+    , substitute+    , substitutePairs+    , convertFOF+    , toPropositional+    , disj+    , conj+    , showFirstOrder+    , prettyFirstOrder+    ) where++import Data.Function (on)+import Data.Generics (Data, Typeable)+import Data.List (intercalate, intersperse)+import Data.Logic.Classes.Arity+import Data.Logic.Classes.Boolean+import Data.Logic.Classes.Logic+import Data.Logic.Classes.Pred+import Data.Logic.Classes.Propositional+import Data.Logic.Classes.Term+import Data.Monoid (mappend)+import Data.SafeCopy (base, deriveSafeCopy)+import qualified Data.Set as S+import Happstack.Data (deriveNewData)+import Text.PrettyPrint (Doc, (<>), (<+>), text, empty, parens, hcat, nest)++-- |The 'FirstOrderFormula' type class.  Minimal implementation:+-- @for_all, exists, foldFirstOrder, foldTerm, (.=.), pApp0-pApp7, fApp, var@.  The+-- functional dependencies are necessary here so we can write+-- functions that don't fix all of the type parameters.  For example,+-- without them the univquant_free_vars function gives the error @No+-- instance for (FirstOrderFormula Formula term V p f)@ because the+-- function doesn't mention the Term type.+class ( Term term v f+      , Pred p term formula+      , Logic formula  -- Basic logic operations+      , Data formula   -- Allows us to use Data.Generics functions on formulas+      , Show v+      , Data p+      , Boolean p      -- To implement true and false below+      , Arity p        -- To decide how many arguments+      , Eq p           -- Required during resolution+      , Ord p+      , Show p+      -- , Pretty p+      , Ord f+      , Show f+      ) => FirstOrderFormula formula term v p f+                                    | formula -> term+                                    , formula -> v+                                    , formula -> p+                                    , formula -> f+                                    , term -> p where+    -- | Universal quantification - for all x (formula x)+    for_all :: v -> formula -> formula+    -- | Existential quantification - there exists x such that (formula x)+    exists ::  v -> formula -> formula++    -- | A fold function similar to the one in 'PropositionalFormula'+    -- but extended to cover both the existing formula types and the+    -- ones introduced here.  @foldFirstOrder (.~.) quant binOp infixPred pApp@+    -- is a no op.  The argument order is taken from Logic-TPTP.+    foldFirstOrder :: (Quant -> v -> formula -> r)+                   -> (Combine formula -> r)+                   -> (Predicate p term -> r)+                   -> formula+                   -> r+    zipFirstOrder :: (Quant -> v -> formula -> Quant -> v -> formula -> Maybe r)+                  -> (Combine formula -> Combine formula -> Maybe r)+                  -> (Predicate p term -> Predicate p term -> Maybe r)+                  -> formula -> formula -> Maybe r++-- |A temporary type used in the fold method to represent the+-- combination of a predicate and its arguments.  This reduces the+-- number of arguments to foldFirstOrder and makes it easier to manage the+-- mapping of the different instances to the class methods.+data Predicate p term+    = Equal term term+    | NotEqual term term+    | Constant Bool+    | Apply p [term]+    deriving (Eq, Ord, Show, Read, Data, Typeable)++-- |for_all with a list of variables, for backwards compatibility.+for_all' :: FirstOrderFormula formula term v p f => [v] -> formula -> formula+for_all' vs f = foldr for_all f vs++-- |exists with a list of variables, for backwards compatibility.+exists' :: FirstOrderFormula formula term v p f => [v] -> formula -> formula+exists' vs f = foldr for_all f vs++-- | Functions to disjunct or conjunct a list.+disj :: FirstOrderFormula formula term v p f => [formula] -> formula+disj [] = false+disj [x] = x+disj (x:xs) = x .|. disj xs++conj :: FirstOrderFormula formula term v p f => [formula] -> formula+conj [] = true+conj [x] = x+conj (x:xs) = x .&. conj xs++-- | Helper function for building folds.+quant :: FirstOrderFormula formula term v p f => +         Quant -> v -> formula -> formula+quant All v f = for_all v f+quant Exists v f = exists v f++-- |Legacy version of quant from when we supported lists of quantified+-- variables.  It also has the virtue of eliding quantifications with+-- empty variable lists (by calling for_all' and exists'.)+quant' :: FirstOrderFormula formula term v p f => +         Quant -> [v] -> formula -> formula+quant' All = for_all'+quant' Exists = exists'++-- |The 'Quant' and 'InfixPred' types, like the BinOp type in+-- 'Data.Logic.Propositional', could be additional parameters to the type+-- class, but it would add additional complexity with unclear+-- benefits.+data Quant = All | Exists deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)++-- |Find the free (unquantified) variables in a formula.+freeVars :: FirstOrderFormula formula term v p f => formula -> S.Set v+freeVars f =+    foldFirstOrder+          (\_ v x -> S.delete v (freeVars x))                    +          (\ cm ->+               case cm of+                 BinOp x _ y -> (mappend `on` freeVars) x y+                 (:~:) f' -> freeVars f')+          (\ pa -> case pa of+                     Constant _ -> S.empty+                     Equal t1 t2 -> S.union (freeVarsOfTerm t1) (freeVarsOfTerm t2)+                     NotEqual t1 t2 -> S.union (freeVarsOfTerm t1) (freeVarsOfTerm t2)+                     Apply _ ts -> S.unions (fmap freeVarsOfTerm ts))+          f+    where+      freeVarsOfTerm = foldTerm S.singleton (\ _ args -> S.unions (fmap freeVarsOfTerm args))++-- | Examine the formula to find the list of outermost universally+-- quantified variables, and call a function with that list and the+-- formula after the quantifiers are removed.+withUnivQuants :: FirstOrderFormula formula term v p f => ([v] -> formula -> r) -> formula -> r+withUnivQuants fn formula =+    doFormula [] formula+    where+      doFormula vs f =+          foldFirstOrder+                (doQuant vs)+                (\ _ -> fn (reverse vs) f)+                (\ _ -> fn (reverse vs) f)+                f+      doQuant vs All v f = doFormula (v : vs) f+      doQuant vs Exists v f = fn (reverse vs) (exists v f)++{-+withImplication :: FirstOrderFormula formula term v p f => r -> (formula -> formula -> r) -> formula -> r+withImplication def fn formula =+    foldFirstOrder (\ _ _ _ -> def) c (\ _ -> def) formula+    where+      c (BinOp a (:=>:) b) = fn a b+      c _ = def+-}++-- |Find the variables that are quantified in a formula+quantVars :: FirstOrderFormula formula term v p f => formula -> S.Set v+quantVars =+    foldFirstOrder+          (\ _ v x -> S.insert v (quantVars x))+          (\ cm ->+               case cm of+                 BinOp x _ y -> (mappend `on` quantVars) x y+                 ((:~:) f) -> quantVars f)+          (\ _ -> S.empty)++-- |Find the free and quantified variables in a formula.+allVars :: FirstOrderFormula formula term v p f => formula -> S.Set v+allVars f =+    foldFirstOrder+          (\_ v x -> S.insert v (allVars x))+          (\ cm ->+               case cm of+                 BinOp x _ y -> (mappend `on` allVars) x y+                 (:~:) f' -> freeVars f')+          (\ pa -> case pa of+                     Equal t1 t2 -> S.union (allVarsOfTerm t1) (allVarsOfTerm t2)+                     NotEqual t1 t2 -> S.union (allVarsOfTerm t1) (allVarsOfTerm t2)+                     Constant _ -> S.empty+                     Apply _ ts -> S.unions (fmap allVarsOfTerm ts))+          f+    where+      allVarsOfTerm = foldTerm S.singleton (\ _ args -> S.unions (fmap allVarsOfTerm args))++-- | Universally quantify all free variables in the formula (Name comes from TPTP)+univquant_free_vars :: FirstOrderFormula formula term v p f => formula -> formula+univquant_free_vars cnf' =+    if S.null free then cnf' else foldr for_all cnf' (S.toList free)+    where free = freeVars cnf'++-- |Replace each free occurrence of variable old with term new.+substitute :: FirstOrderFormula formula term v p f => v -> term -> formula -> formula+substitute old new formula =+    foldTerm (\ new' -> if old == new' then formula else substitute' formula)+             (\ _ _ -> substitute' formula)+             new+    where+      substitute' =+          foldFirstOrder -- If the old variable appears in a quantifier+                -- we can stop doing the substitution.+                (\ q v f' -> quant q v (if old == v then f' else substitute' f'))+                (\ cm -> case cm of+                           ((:~:) f') -> combine ((:~:) (substitute' f'))+                           (BinOp f1 op f2) -> combine (BinOp (substitute' f1) op (substitute' f2)))+                (\ pa -> case pa of+                           Equal t1 t2 -> (st t1) .=. (st t2)+                           NotEqual t1 t2 -> (st t1) .!=. (st t2)+                           Constant x -> pApp0 (fromBool x)+                           Apply p ts -> pApp p (map st ts))+      st t = foldTerm sv (\ func ts -> fApp func (map st ts)) t+      sv v = if v == old then new else var v++substitutePairs :: (FirstOrderFormula formula term v p f) => [(v, term)] -> formula -> formula+substitutePairs pairs formula = foldr (\ (old, new) f -> substitute old new f) formula pairs ++-- |Convert any instance of a first order logic expression to any other.+convertFOF :: forall formula1 term1 v1 p1 f1 formula2 term2 v2 p2 f2.+              (FirstOrderFormula formula1 term1 v1 p1 f1,+               FirstOrderFormula formula2 term2 v2 p2 f2) =>+              (v1 -> v2) -> (p1 -> p2) -> (f1 -> f2) -> formula1 -> formula2+convertFOF convertV convertP convertF formula =+    foldFirstOrder q c p formula+    where+      convert' = convertFOF convertV convertP convertF+      convertTerm' = convertTerm convertV convertF+      q x v f = quant x (convertV v) (convert' f)+      c (BinOp f1 op f2) = combine (BinOp (convert' f1) op (convert' f2))+      c ((:~:) f) = combine ((:~:) (convert' f))+      p (Equal t1 t2) = (convertTerm' t1) .=. (convertTerm' t2)+      p (NotEqual t1 t2) = (convertTerm' t1) .!=. (convertTerm' t2)+      p (Apply x ts) = pApp (convertP x) (map convertTerm' ts)+      p (Constant x) = pApp (fromBool x) []++-- |Names for for_all and exists inspired by the conventions of the+-- TPTP project.+(!) :: FirstOrderFormula formula term v p f => v -> formula -> formula+(!) = for_all+(?) :: FirstOrderFormula formula term v p f => v -> formula -> formula+(?) = exists++-- |Try to convert a first order logic formula to propositional.  This+-- will return Nothing if there are any quantifiers, or if it runs+-- into an atom that it is unable to convert.+toPropositional :: forall formula1 term v p f formula2 atom.+                   (FirstOrderFormula formula1 term v p f,+                    PropositionalFormula formula2 atom) =>+                   (formula1 -> formula2) -> formula1 -> formula2+toPropositional convertAtom formula =+    foldFirstOrder q c p formula+    where+      convert' = toPropositional convertAtom+      q _ _ _ = error "toPropositional: invalid argument"+      c (BinOp f1 op f2) = combine (BinOp (convert' f1) op (convert' f2))+      c ((:~:) f) = combine ((:~:) (convert' f))+      p _ = convertAtom formula++-- | Display a formula in a format that can be read into the interpreter.+showFirstOrder :: forall formula term v p f. (FirstOrderFormula formula term v p f, Show v, Show p, Show f) => +                  formula -> String+showFirstOrder formula =+    foldFirstOrder q c a formula+    where+      q All v f = "(for_all " ++ show v ++ " " ++ showFirstOrder f ++ ")"+      q Exists v f = "(exists " ++  show v ++ " " ++ showFirstOrder f ++ ")"+      c (BinOp f1 op f2) = "(" ++ parenForm f1 ++ " " ++ showCombine op ++ " " ++ parenForm f2 ++ ")"+      c ((:~:) f) = "((.~.) " ++ showFirstOrder f ++ ")"+      a :: Predicate p term -> String+      a (Equal t1 t2) =+          "(" ++ parenTerm t1 ++ " .=. " ++ parenTerm t2 ++ ")"+      a (NotEqual t1 t2) =+          "(" ++ parenTerm t1 ++ " .!=. " ++ parenTerm t2 ++ ")"+      a (Constant x) = "pApp' (Constant " ++ show x ++ ")"+      a (Apply p ts) = "(pApp" ++ show (length ts) ++ " (" ++ show p ++ ") (" ++ intercalate ") (" (map showTerm ts) ++ "))"+      parenForm x = "(" ++ showFirstOrder x ++ ")"+      parenTerm :: term -> String+      parenTerm x = "(" ++ showTerm x ++ ")"+      showCombine (:<=>:) = ".<=>."+      showCombine (:=>:) = ".=>."+      showCombine (:&:) = ".&."+      showCombine (:|:) = ".|."++prettyFirstOrder :: forall formula term v p f. (FirstOrderFormula formula term v p f) =>+                    (v -> Doc)+                 -> (p -> Doc)+                 -> (f -> Doc)+                 -> Int+                 -> formula+                 -> Doc+prettyFirstOrder pv pp pf prec formula =+    foldFirstOrder+          (\ qop v f -> parensIf (prec > 1) $ prettyQuant qop <> pv v <+> prettyFirstOrder pv pp pf 1 f)+          (\ cm ->+               case cm of+                 (BinOp f1 op f2) ->+                     case op of+                       (:=>:) -> parensIf (prec > 2) $ (prettyFirstOrder pv pp pf 2 f1 <+> formOp op <+> prettyFirstOrder pv pp pf 2 f2)+                       (:<=>:) -> parensIf (prec > 2) $ (prettyFirstOrder pv pp pf 2 f1 <+> formOp op <+> prettyFirstOrder pv pp pf 2 f2)+                       (:&:) -> parensIf (prec > 3) $ (prettyFirstOrder pv pp pf 3 f1 <+> formOp op <+> prettyFirstOrder pv pp pf 3 f2)+                       (:|:) -> parensIf {-(prec > 4)-} True $ (prettyFirstOrder pv pp pf 4 f1 <+> formOp op <+> prettyFirstOrder pv pp pf 4 f2)+                 ((:~:) f) -> text {-"¬"-} "~" <> prettyFirstOrder pv pp pf 5 f)+          pr+          formula+    where+      pr :: Predicate p term -> Doc+      pr (Constant x) = text (show x)+      pr (Equal t1 t2) = parensIf (prec > 6) (prettyTerm pv pf t1 <+> text "=" <+> prettyTerm pv pf t2)+      pr (NotEqual t1 t2) = parensIf (prec > 6) (prettyTerm pv pf t1 <+> text "!=" <+> prettyTerm pv pf t2)+      pr (Apply p ts) =+          pp p <> case ts of+                    [] -> empty+                    _ -> parens (hcat (intersperse (text ",") (map (prettyTerm pv pf) ts)))+      parensIf False = id+      parensIf _ = parens . nest 1+      prettyQuant All = text {-"∀"-} "!"+      prettyQuant Exists = text {-"∃"-} "?"+      formOp (:<=>:) = text "<=>"+      formOp (:=>:) = text "=>"+      formOp (:&:) = text "&"+      formOp (:|:) = text "|"++$(deriveSafeCopy 1 'base ''Quant)+$(deriveSafeCopy 1 'base ''Predicate)++$(deriveNewData [''Quant])+$(deriveNewData [''Predicate])
+ Data/Logic/Classes/Literal.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wwarn #-}+module Data.Logic.Classes.Literal+    ( Literal(..)+    , PredicateLit(..)+    , fromFirstOrder+    , prettyLit+    ) where++import Data.Generics (Data)+import Data.List (intersperse)+import Data.Logic.Classes.Boolean+import Data.Logic.Classes.FirstOrder+import Data.Logic.Classes.Negatable+import Data.Logic.Classes.Propositional (Combine(..))+import Data.Logic.Classes.Term+import Text.PrettyPrint (Doc, (<>), (<+>), text, empty, parens, hcat, nest)++-- |Literals are the building blocks of the clause and implicative normal+-- |forms.  They support negation and must include True and False elements.+class ( Ord lit+      , Eq p+      , Ord p+      , Boolean p+      , Term term v f+      , Negatable lit+      , Data lit+      , Show lit+      ) => Literal lit term v p f | lit -> term, lit -> v, lit -> p, lit -> f where+    equals :: term -> term -> lit+    pAppLiteral :: p -> [term] -> lit+    foldLiteral :: (lit -> r) -> (PredicateLit p term -> r) -> lit -> r+    zipLiterals :: (lit -> lit -> Maybe r) -> (PredicateLit p term -> PredicateLit p term -> Maybe r) -> lit -> lit -> Maybe r++-- |Helper type to implement the fold function for 'Literal'.+data PredicateLit p term+    = ApplyLit p [term]+    | EqualLit term term++-- |Just like Logic.FirstOrder.convertFOF except it rejects anything+-- with a construct unsupported in a normal logic formula,+-- i.e. quantifiers and formula combinators other than negation.+fromFirstOrder :: forall formula term v p f lit term2 v2 p2 f2.+                  (FirstOrderFormula formula term v p f, Literal lit term2 v2 p2 f2) =>+                  (v -> v2) -> (p -> p2) -> (f -> f2) -> formula -> lit+fromFirstOrder cv cp cf formula =+    foldFirstOrder (\ _ _ _ -> error "toLiteral q") c p formula+    where+      c :: Combine formula -> lit+      c ((:~:) f) =  (.~.) (fromFirstOrder cv cp cf f)+      c _ = error "fromFirstOrder"+      p :: Predicate p term -> lit+      p (Equal a b) = ct a `equals` ct b+      p (NotEqual a b) = (.~.) (ct a `equals` ct b)+      p (Apply pr ts) = pAppLiteral (cp pr) (map ct ts)+      p (Constant b) = error $ "fromFirstOrder " ++ show b+      ct = convertTerm cv cf++prettyLit :: forall lit term v p f. (Literal lit term v p f) =>+              (v -> Doc)+           -> (p -> Doc)+           -> (f -> Doc)+           -> Int+           -> lit+           -> Doc+prettyLit pv pp pf prec lit =+    foldLiteral c p lit+    where+      c x = if negated x then text {-"¬"-} "~" <> prettyLit pv pp pf 5 x else prettyLit pv pp pf 5 x+      p (ApplyLit pr ts) =+          pp pr <> case ts of+                        [] -> empty+                        _ -> parens (hcat (intersperse (text ",") (map (prettyTerm pv pf) ts)))+      p (EqualLit t1 t2) = parensIf (prec > 6) (prettyTerm pv pf t1 <+> text "=" <+> prettyTerm pv pf t2)+      parensIf False = id+      parensIf _ = parens . nest 1
+ Data/Logic/Classes/Logic.hs view
@@ -0,0 +1,43 @@+-- | Class Logic defines the basic boolean logic operations,+-- AND, OR, NOT, and so on.  Definitions which pertain to both+-- propositional and first order logic are here.+module Data.Logic.Classes.Logic where++import Data.Logic.Classes.Negatable++-- |A type class for logical formulas.  Minimal implementation:+-- @+--  (.|.), (.~.)+-- @+class (Negatable formula, Ord formula) => Logic formula where+    -- | Disjunction/OR+    (.|.) :: formula -> formula -> formula++    -- | Derived formula combinators.  These could (and should!) be+    -- overridden with expressions native to the instance.+    --+    -- | Conjunction/AND+    (.&.) :: formula -> formula -> formula+    x .&. y = (.~.) ((.~.) x .|. (.~.) y)+    -- | Formula combinators: Equivalence+    (.<=>.) :: formula -> formula -> formula+    x .<=>. y = (x .=>. y) .&. (y .=>. x)+    -- | Implication+    (.=>.) :: formula -> formula -> formula+    x .=>. y = ((.~.) x .|. y)+    -- | Reverse implication:+    (.<=.) :: formula -> formula -> formula+    x .<=. y = y .=>. x+    -- | Exclusive or+    (.<~>.) :: formula -> formula -> formula+    x .<~>. y = ((.~.) x .&. y) .|. (x .&. (.~.) y)+    -- | Nor+    (.~|.) :: formula -> formula -> formula+    x .~|. y = (.~.) (x .|. y)+    -- | Nand+    (.~&.) :: formula -> formula -> formula+    x .~&. y = (.~.) (x .&. y)++infixl 2  .<=>. ,  .=>. ,  .<~>.+infixl 3  .&.+infixl 4  .|.  -- a & b | c means a & (b | c), which in cnf would be [[a], [b, c]]
+ Data/Logic/Classes/Negatable.hs view
@@ -0,0 +1,10 @@+module Data.Logic.Classes.Negatable where++-- |The class of formulas that can be negated.  There are some types+-- that can be negated but do not support the other Boolean Logic+-- operators, such as the 'Literal' class.+class Negatable formula where+    -- | Is this negated at the top level?+    negated :: formula -> Bool+    -- | Negation (This needs to check for and remove double negation)+    (.~.) :: formula -> formula
+ Data/Logic/Classes/Pred.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses, ScopedTypeVariables #-}+module Data.Logic.Classes.Pred where++import Data.Logic.Classes.Arity+import Data.Logic.Classes.Boolean+import Data.Logic.Classes.Logic+import Data.Logic.Classes.Negatable++-- |A class of predicates+class (Logic formula, Boolean p, Arity p) => Pred p term formula | formula -> p, formula -> term where+    pApp0 :: p  -> formula+    pApp1 :: p -> term -> formula+    pApp2 :: p -> term -> term -> formula+    pApp3 :: p -> term -> term -> term -> formula+    pApp4 :: p -> term -> term -> term -> term -> formula+    pApp5 :: p -> term -> term -> term -> term -> term -> formula+    pApp6 :: p -> term -> term -> term -> term -> term -> term -> formula+    pApp7 :: p -> term -> term -> term -> term -> term -> term -> term -> formula+    -- | Equality of Terms+    (.=.) :: term -> term -> formula+    -- | Inequality of Terms+    (.!=.) :: term -> term -> formula+    a .!=. b = (.~.) (a .=. b)+    -- | The tautological formula+    true :: formula+    true = pApp0 (fromBool True :: p)+    -- | The inconsistant formula+    false :: formula+    false = pApp0 (fromBool False :: p)++pApp :: (Pred p term formula, Arity p) => p -> [term] -> formula+pApp p ts =+    case (ts, maybe (length ts) id (arity p)) of+      ([], 0) -> pApp0 p +      ([a], 1) -> pApp1 p a+      ([a,b], 2) -> pApp2 p a b+      ([a,b,c], 3) -> pApp3 p a b c+      ([a,b,c,d], 4) -> pApp4 p a b c d+      ([a,b,c,d,e], 5) -> pApp5 p a b c d e+      ([a,b,c,d,e,f], 6) -> pApp6 p a b c d e f+      ([a,b,c,d,e,f,g], 7) -> pApp7 p a b c d e f g+      _ -> error ("Arity error" {- ++ show (pretty p) ++ " " ++ intercalate " " (map (show . pretty) ts) -})
+ Data/Logic/Classes/Propositional.hs view
@@ -0,0 +1,324 @@+-- | PropositionalFormula is a multi-parameter type class for+-- representing instance of propositional (aka zeroth order) logic+-- datatypes.  These are formulas which have truth values, but no "for+-- all" or "there exists" quantifiers and thus no variables or terms+-- as we have in first order or predicate logic.  It is intended that+-- we will be able to write instances for various different+-- implementations to allow these systems to interoperate.  The+-- operator names were adopted from the Logic-TPTP package.+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, FunctionalDependencies,+             MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, UndecidableInstances #-}+module Data.Logic.Classes.Propositional+    ( PropositionalFormula(..)+    , showPropositional+    , convertProp+    , BinOp(..)+    , Combine(..)+    , combine+    , negationNormalForm+    , clauseNormalForm+    , clauseNormalForm'+    , clauseNormalFormAlt+    , clauseNormalFormAlt'+    , disjunctiveNormalForm+    , disjunctiveNormalForm'+    ) where++import Data.Generics (Data, Typeable)+import Data.Logic.Classes.Boolean+import Data.Logic.Classes.Negatable+import Data.Logic.Classes.Logic+import Data.SafeCopy (base, deriveSafeCopy)+import qualified Data.Set.Extra as Set+import Happstack.Data (deriveNewData)++-- |A type class for propositional logic.  If the type we are writing+-- an instance for is a zero-order (aka propositional) logic type+-- there will generally by a type or a type parameter corresponding to+-- atom.  For first order or predicate logic types, it is generally+-- easiest to just use the formula type itself as the atom type, and+-- raise errors in the implementation if a non-atomic formula somehow+-- appears where an atomic formula is expected (i.e. as an argument to+-- atomic or to the third argument of foldPropositional.)+class (Logic formula, Boolean formula, Ord formula, Ord atom) => PropositionalFormula formula atom | formula -> atom where+    -- | Build an atomic formula from the atom type.+    atomic :: atom -> formula+    -- | A fold function that distributes different sorts of formula+    -- to its parameter functions, one to handle binary operators, one+    -- for negations, and one for atomic formulas.  See examples of its+    -- use to implement the polymorphic functions below.+    foldPropositional :: (Combine formula -> r)+                      -> (atom -> r)+                      -> formula+                      -> r++-- | Show a formula in a format that can be evaluated +showPropositional :: (PropositionalFormula formula atom) => (atom -> String) -> formula -> String+showPropositional showAtom formula =+    foldPropositional c a formula+    where+      c ((:~:) f) = "(.~.) " ++ parenForm f+      c (BinOp f1 op f2) = parenForm f1 ++ " " ++ showFormOp op ++ " " ++ parenForm f2+      a = showAtom+      parenForm x = "(" ++ showPropositional showAtom x ++ ")"+      showFormOp (:<=>:) = ".<=>."+      showFormOp (:=>:) = ".=>."+      showFormOp (:&:) = ".&."+      showFormOp (:|:) = ".|."++-- |Convert any instance of a propositional logic expression to any+-- other using the supplied atom conversion function.+convertProp :: forall formula1 atom1 formula2 atom2.+               (PropositionalFormula formula1 atom1,+                PropositionalFormula formula2 atom2) =>+               (atom1 -> atom2) -> formula1 -> formula2+convertProp convertA formula =+    foldPropositional c a formula+    where+      convert' = convertProp convertA+      c ((:~:) f) = (.~.) (convert' f)+      c (BinOp f1 op f2) = combine (BinOp (convert' f1) op (convert' f2))+      a = atomic . convertA++-- |'Combine' is a helper type used in the signatures of the+-- 'foldPropositional' and 'foldFirstOrder' methods so can represent+-- all the ways that formulas can be combined using boolean logic -+-- negation, logical And, and so forth.+data Combine formula+    = BinOp formula BinOp formula+    | (:~:) formula+    deriving (Eq,Ord,Read,Data,Typeable)++-- | Represents the boolean logic binary operations, used in the+-- Combine type above.+data BinOp+    = (:<=>:)  -- ^ Equivalence+    |  (:=>:)  -- ^ Implication+    |  (:&:)  -- ^ AND+    |  (:|:)  -- ^ OR+    deriving (Eq,Ord,Read,Data,Typeable,Enum,Bounded)++-- |We need to implement read manually here due to+-- <http://hackage.haskell.org/trac/ghc/ticket/4136>+{-+instance Read BinOp where+    readsPrec _ s = +        map (\ (x, t) -> (x, drop (length t) s))+            (take 1 (dropWhile (\ (_, t) -> not (isPrefixOf t s)) prs))+        where+          prs = [((:<=>:), ":<=>:"),+                 ((:=>:), ":=>:"),+                 ((:&:), ":&:"),+                 ((:|:), ":|:")]+-}++instance Show BinOp where+    show (:<=>:) = "(:<=>:)"+    show (:=>:) = "(:=>:)"+    show (:&:) = "(:&:)"+    show (:|:) = "(:|:)"++-- | A helper function for building folds:+-- @+--   foldPropositional combine atomic+-- @+-- is a no-op.+combine :: Logic formula => Combine formula -> formula+combine (BinOp f1 (:<=>:) f2) = f1 .<=>. f2+combine (BinOp f1 (:=>:) f2) = f1 .=>. f2+combine (BinOp f1 (:&:) f2) = f1 .&. f2+combine (BinOp f1 (:|:) f2) = f1 .|. f2+combine ((:~:) f) = (.~.) f++-- | Simplify and recursively apply nnf.+negationNormalForm :: PropositionalFormula formula atom => formula -> formula+negationNormalForm = nnf . psimplify++-- |Eliminate => and <=> and move negations inwards:+-- +-- @+-- Formula      Rewrites to+--  P => Q      ~P | Q+--  P <=> Q     (P & Q) | (~P & ~Q)+-- ~∀X P        ∃X ~P+-- ~∃X P        ∀X ~P+-- ~(P & Q)     (~P | ~Q)+-- ~(P | Q)     (~P & ~Q)+-- ~~P  P+-- @+-- +nnf :: PropositionalFormula formula atom => formula -> formula+nnf fm =+    foldPropositional (nnfCombine fm) (\ _ -> fm) fm++nnfCombine :: PropositionalFormula r atom => r -> Combine r -> r+nnfCombine fm ((:~:) p) = foldPropositional nnfNotCombine (\ _ -> fm) p+nnfCombine _ (BinOp p (:=>:) q) = nnf ((.~.) p) .|. (nnf q)+nnfCombine _ (BinOp p (:<=>:) q) =  (nnf p .&. nnf q) .|. (nnf ((.~.) p) .&. nnf ((.~.) q))+nnfCombine _ (BinOp p (:&:) q) = nnf p .&. nnf q+nnfCombine _ (BinOp p (:|:) q) = nnf p .|. nnf q++nnfNotCombine :: PropositionalFormula formula atom => Combine formula -> formula+nnfNotCombine ((:~:) p) = nnf p+nnfNotCombine (BinOp p (:&:) q) = nnf ((.~.) p) .|. nnf ((.~.) q)+nnfNotCombine (BinOp p (:|:) q) = nnf ((.~.) p) .&. nnf ((.~.) q)+nnfNotCombine (BinOp p (:=>:) q) = nnf p .&. nnf ((.~.) q)+nnfNotCombine (BinOp p (:<=>:) q) = (nnf p .&. nnf ((.~.) q)) .|. nnf ((.~.) p) .&. nnf q++-- |Do a bottom-up recursion to simplify a propositional formula.+psimplify :: PropositionalFormula formula atom => formula -> formula+psimplify fm =+    foldPropositional c a fm+    where+      c ((:~:) p) = psimplify1 ((.~.) (psimplify p))+      c (BinOp p (:&:) q) = psimplify1 (psimplify p .&. psimplify q)+      c (BinOp p (:|:) q) = psimplify1 (psimplify p .|. psimplify q)+      c (BinOp p (:=>:) q) = psimplify1 (psimplify p .=>. psimplify q)+      c (BinOp p (:<=>:) q) = psimplify1 (psimplify p .<=>. psimplify q)+      a _ = fm++-- |Do one step of simplify for propositional formulas:+-- Perform the following transformations everywhere, plus any+-- commuted versions for &, |, and <=>.+-- +-- @+--  ~False      -> True+--  ~True       -> False+--  True & P    -> P+--  False & P   -> False+--  True | P    -> True+--  False | P   -> P+--  True => P   -> P+--  False => P  -> True+--  P => True   -> P+--  P => False  -> True+--  True <=> P  -> P+--  False <=> P -> ~P+-- @+-- +psimplify1 :: forall formula atom. PropositionalFormula formula atom => formula -> formula+psimplify1 fm =+    foldPropositional simplifyCombine (\ _ -> fm) fm+    where+      simplifyCombine ((:~:) f) = foldPropositional simplifyNotCombine simplifyNotAtom f+      simplifyCombine (BinOp l op r) =+          case (asBool l, op, asBool r) of+            (Just True,  (:&:), _)            -> r+            (Just False, (:&:), _)            -> fromBool False+            (_,          (:&:), Just True)    -> l+            (_,          (:&:), Just False)   -> fromBool False+            (Just True,  (:|:), _)            -> fromBool True+            (Just False, (:|:), _)            -> r+            (_,          (:|:), Just True)    -> fromBool True+            (_,          (:|:), Just False)   -> l+            (Just True,  (:=>:), _)           -> r+            (Just False, (:=>:), _)           -> fromBool True+            (_,          (:=>:), Just True)   -> fromBool True+            (_,          (:=>:), Just False)  -> (.~.) l+            (Just True,  (:<=>:), _)          -> r+            (Just False, (:<=>:), _)          -> (.~.) r+            (_,          (:<=>:), Just True)  -> l+            (_,          (:<=>:), Just False) -> (.~.) l+            _                                 -> fm+      simplifyNotCombine ((:~:) f) = f+      simplifyNotCombine _ = fm+      simplifyNotAtom x = (.~.) (atomic x)+      -- We don't require an Eq instance, but we do require Ord so that+      -- we can make sets.+      asBool :: formula -> Maybe Bool+      asBool x =+          case compare x (fromBool True) of+            EQ -> Just True+            _ -> case compare x (fromBool False) of+                   EQ -> Just False+                   _ -> Nothing++clauseNormalForm' :: (PropositionalFormula formula atom) => formula -> Set.Set (Set.Set formula)+clauseNormalForm' = simp purecnf . negationNormalForm++clauseNormalForm :: forall formula atom. (PropositionalFormula formula atom) => formula -> formula+clauseNormalForm formula =+    case clean (lists cnf) of+      [] -> fromBool True+      xss -> foldr1 (.&.) . map (foldr1 (.|.)) $ xss+    where+      clean = filter (not . null)+      lists = Set.toList . Set.map Set.toList+      cnf = clauseNormalForm' formula++-- |I'm not sure of the clauseNormalForm functions above are wrong or just different.+clauseNormalFormAlt' :: (PropositionalFormula formula atom) => formula -> Set.Set (Set.Set formula)+clauseNormalFormAlt' = simp purecnf' . negationNormalForm++clauseNormalFormAlt :: forall formula atom. (PropositionalFormula formula atom) => formula -> formula+clauseNormalFormAlt formula =+    case clean (lists cnf) of+      [] -> fromBool True+      xss -> foldr1 (.&.) . map (foldr1 (.|.)) $ xss+    where+      clean = filter (not . null)+      lists = Set.toList . Set.map Set.toList+      cnf = clauseNormalFormAlt' formula++disjunctiveNormalForm :: (PropositionalFormula formula atom) => formula -> formula+disjunctiveNormalForm formula =+    case clean (lists dnf) of+      [] -> fromBool False+      xss -> foldr1 (.|.) . map (foldr1 (.&.)) $ xss+    where+      clean = filter (not . null)+      lists = Set.toList . Set.map Set.toList+      dnf = disjunctiveNormalForm' formula++disjunctiveNormalForm' :: (PropositionalFormula formula atom) => formula -> Set.Set (Set.Set formula)+disjunctiveNormalForm' = simp purednf . negationNormalForm++simp :: forall formula atom. (PropositionalFormula formula atom) =>+        (formula -> Set.Set (Set.Set formula)) -> formula -> Set.Set (Set.Set formula)+simp purenf fm =+    case (compare fm (fromBool False), compare fm (fromBool True)) of+      (EQ, _) -> Set.empty+      (_, EQ) -> Set.singleton Set.empty+      _ ->cjs'+    where+      -- Discard any clause that is the proper subset of another clause+      cjs' = Set.filter keep cjs+      keep x = not (Set.or (Set.map (Set.isProperSubsetOf x) cjs))+      cjs = Set.filter (not . trivial) (purenf (nnf fm)) :: Set.Set (Set.Set formula)++-- |Harrison page 59.  Look for complementary pairs in a clause.+trivial :: (Negatable lit, Ord lit) => Set.Set lit -> Bool+trivial lits =+    not . Set.null $ Set.intersection (Set.map (.~.) n) p+    where (n, p) = Set.partition negated lits++--purecnf :: forall formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f) => formula -> Set.Set (Set.Set lit)+purecnf :: forall formula atom. PropositionalFormula formula atom => formula -> Set.Set (Set.Set formula)+purecnf fm = Set.map (Set.map (.~.)) (purednf (nnf ((.~.) fm)))++purednf :: forall formula atom. (PropositionalFormula formula atom) => formula -> Set.Set (Set.Set formula)+purednf fm =+    foldPropositional c (\ _ -> x)  fm+    where+      c :: Combine formula -> Set.Set (Set.Set formula)+      c (BinOp p (:&:) q) = Set.distrib (purednf p) (purednf q)+      c (BinOp p (:|:) q) = Set.union (purednf p) (purednf q)+      c _ = x+      x :: Set.Set (Set.Set formula)+      x = Set.singleton (Set.singleton (convertProp id fm)) :: Set.Set (Set.Set formula)++purecnf' :: forall formula atom. (PropositionalFormula formula atom) => formula -> Set.Set (Set.Set formula)+purecnf' fm =+    foldPropositional c (\ _ -> x)  fm+    where+      c :: Combine formula -> Set.Set (Set.Set formula)+      c (BinOp p (:&:) q) = Set.union (purecnf' p) (purecnf' q)+      c (BinOp p (:|:) q) = Set.distrib (purecnf' p) (purecnf' q)+      c _ = x+      x :: Set.Set (Set.Set formula)+      x = Set.singleton (Set.singleton (convertProp id fm)) :: Set.Set (Set.Set formula)++$(deriveSafeCopy 1 'base ''BinOp)+$(deriveSafeCopy 1 'base ''Combine)++$(deriveNewData [''BinOp, ''Combine])
+ Data/Logic/Classes/Skolem.hs view
@@ -0,0 +1,7 @@+module Data.Logic.Classes.Skolem where++-- |This class shows how to convert between atomic Skolem functions+-- and Ints.+class Skolem f where+    toSkolem :: Int -> f+    fromSkolem  :: f -> Maybe Int
+ Data/Logic/Classes/Term.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables #-}+module Data.Logic.Classes.Term+    ( Term(..)+    , convertTerm+    , showTerm+    , prettyTerm+    ) where++import Data.Generics (Data)+import Data.List (intercalate, intersperse)+import Data.Logic.Classes.Skolem+import Data.Logic.Classes.Variable+import Text.PrettyPrint (Doc, (<>), brackets, hcat, text)++class ( Ord v     -- Required so variables can be inserted into maps and sets+      , Variable v -- Used to rename variable during conversion to prenex+      , Data v    -- For serialization+      , Eq f      -- We need to check functions for equality during unification+      , Skolem f  -- Used to create skolem functions and constants+      , Data f    -- For serialization+      , Ord term  -- For implementing Ord in Literal+      ) => Term term v f | term -> v, term -> f where+    var :: v -> term+    -- ^ Build a term which is a variable reference.+    fApp :: f -> [term] -> term+    -- ^ Build a term by applying terms to an atomic function.  @f@+    -- (atomic function) is one of the type parameters, this package+    -- is mostly indifferent to its internal structure.+    foldTerm :: (v -> r) -> (f -> [term] -> r) -> term -> r+    -- ^ A fold for the term data type, which understands terms built+    -- from a variable and a term built from the application of a+    -- primitive function to other terms.+    zipT :: (v -> v -> Maybe r) -> (f -> [term] -> f -> [term] -> Maybe r) -> term -> term -> Maybe r++convertTerm :: forall term1 v1 f1 term2 v2 f2.+               (Term term1 v1 f1,+                Term term2 v2 f2) =>+               (v1 -> v2) -> (f1 -> f2) -> term1 -> term2+convertTerm convertV convertF term =+    foldTerm v fn term+    where+      convertTerm' = convertTerm convertV convertF+      v = var . convertV+      fn x ts = fApp (convertF x) (map convertTerm' ts)++showTerm :: forall term v f. (Term term v f, Show v, Show f) =>+            term -> String+showTerm term =+    foldTerm v f term+    where+      v :: v -> String+      v v' = "var (" ++ show v' ++ ")"+      f :: f -> [term] -> String+      f fn ts = "fApp (" ++ show fn ++ ") [" ++ intercalate "," (map showTerm ts) ++ "]"++prettyTerm :: forall v f term. (Term term v f) =>+              (v -> Doc)+           -> (f -> Doc)+           -> term+           -> Doc+prettyTerm pv pf t = foldTerm pv (\ fn ts -> pf fn <> brackets (hcat (intersperse (text ",") (map (prettyTerm pv pf) ts)))) t
+ Data/Logic/Classes/Variable.hs view
@@ -0,0 +1,23 @@+module Data.Logic.Classes.Variable+    ( Variable(one, next)+    , variant+    ) where++import qualified Data.Set as S++-- |A class for finding unused variable names.  The next method+-- returns the next in an endless sequence of variable names, if we+-- keep calling it we are bound to find some unused name.+class Variable v where+    one :: v+    -- ^ Return some commonly used variable, typically x+    next :: v -> v+    -- ^ Return a different variable name, @iterate next one@ should+    -- return a list which never repeats.++-- |Find a variable name which is not in the variables set which is+-- stored in the monad.  This is initialized above with the free+-- variables in the formula.  (FIXME: this is not worth putting in+-- a monad, just pass in the set of free variables.)+variant :: (Variable v, Ord v) => S.Set v -> v -> v+variant names x = if S.member x names then variant names (next x) else x
+ Data/Logic/Instances/Chiou.hs view
@@ -0,0 +1,272 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,+             RankNTypes, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall -Werror -fno-warn-orphans -fno-warn-missing-signatures #-}+module Data.Logic.Instances.Chiou+    ( Sentence(..)+    , CTerm(..)+    , Connective(..)+    , Quantifier(..)+    , ConjunctiveNormalForm(..)+    , NormalSentence(..)+    , NormalTerm(..)+    , toSentence+    , fromSentence+    ) where++import Data.Generics (Data, Typeable)+import Data.Logic.Classes.Arity (Arity)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), Quant(..), quant')+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Classes.Term as Logic+import qualified Data.Logic.Classes.FirstOrder as L+import Data.Logic.Classes.Propositional (PropositionalFormula(..), BinOp(..), Combine(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Variable (Variable)+import Data.String (IsString(..))++data Sentence v p f+    = Connective (Sentence v p f) Connective (Sentence v p f)+    | Quantifier Quantifier [v] (Sentence v p f)+    | Not (Sentence v p f)+    | Predicate p [CTerm v f]+    | Equal (CTerm v f) (CTerm v f)+    deriving (Eq, Ord, Data, Typeable)++data CTerm v f+    = Function f [CTerm v f]+    | Variable v+    deriving (Eq, Ord, Data, Typeable)++data Connective+    = Imply+    | Equiv+    | And+    | Or+    deriving (Eq, Ord, Show, Data, Typeable)++data Quantifier+    = ForAll+    | ExistsCh+    deriving (Eq, Ord, Show, Data, Typeable)++instance Negatable (Sentence v p f) where+    (.~.) (Not (Not x)) = (.~.) x+    (.~.) (Not x) = x+    (.~.) x   = Not x+    negated (Not x) = not (negated x)+    negated _ = False++instance (Ord v, Ord p, Ord f) => Logic (Sentence v p f) where+    x .<=>. y = Connective x Equiv y+    x .=>.  y = Connective x Imply y+    x .|.   y = Connective x Or y+    x .&.   y = Connective x And y++instance (Ord v, IsString v, Data v, Variable v, +          Ord p, IsString p, Data p, Boolean p, Arity p,+          Ord f, IsString f, Data f, Skolem f, +          Boolean (Sentence v p f), Logic (Sentence v p f)) =>+         PropositionalFormula (Sentence v p f) (Sentence v p f) where+    atomic (Connective _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic (Quantifier _ _ _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic (Not _) = error "Logic.Instances.Chiou.atomic: unexpected"+    atomic (Predicate p ts) = pApp p ts+    atomic (Equal t1 t2) = t1 .=. t2+    foldPropositional c a formula =+        case formula of+          Not x -> c ((:~:) x)+          Quantifier _ _ _ -> error "Logic.Instance.Chiou.foldF0: unexpected"+          Connective f1 Imply f2 -> c (BinOp f1 (:=>:) f2)+          Connective f1 Equiv f2 -> c (BinOp f1 (:<=>:) f2)+          Connective f1 And f2 -> c (BinOp f1 (:&:) f2)+          Connective f1 Or f2 -> c (BinOp f1 (:|:) f2)+          Predicate p ts -> a (Predicate p ts)+          Equal t1 t2 -> a (Equal t1 t2)++data AtomicFunction+    = AtomicFunction String+    -- This is redundant with the SkolemFunction and SkolemConstant+    -- constructors in the Chiou Term type.+    | AtomicSkolemFunction Int+    deriving (Eq, Show)++instance IsString AtomicFunction where+    fromString = AtomicFunction++instance Skolem AtomicFunction where+    toSkolem = AtomicSkolemFunction +    fromSkolem (AtomicSkolemFunction n) = Just n+    fromSkolem _ = Nothing++instance (Ord v, Ord p, Arity p, Boolean p, Ord f) => Pred p (CTerm v f) (Sentence v p f) where+    pApp0 x = Predicate x []+    pApp1 x a = Predicate x [a]+    pApp2 x a b = Predicate x [a,b]+    pApp3 x a b c = Predicate x [a,b,c]+    pApp4 x a b c d = Predicate x [a,b,c,d]+    pApp5 x a b c d e = Predicate x [a,b,c,d,e]+    pApp6 x a b c d e f = Predicate x [a,b,c,d,e,f]+    pApp7 x a b c d e f g = Predicate x [a,b,c,d,e,f,g]+    -- fApp (AtomicSkolemFunction n) [] = SkolemConstant n+    -- fApp (AtomicSkolemFunction n) ts = SkolemFunction n ts+    x .=. y = Equal x y++instance (Ord v, IsString v, Variable v, Data v, Show v,+          Ord p, IsString p, Boolean p, Arity p, Data p, Show p,+          Ord f, IsString f, Skolem f, Data f, Show f,+          PropositionalFormula (Sentence v p f) (Sentence v p f)) =>+          FirstOrderFormula (Sentence v p f) (CTerm v f) v p f where+    for_all v x = Quantifier ForAll [v] x+    exists v x = Quantifier ExistsCh [v] x+    foldFirstOrder q c p f =+        case f of+          Not x -> c ((:~:) x)+          Quantifier op (v:vs) f' ->+              let op' = case op of+                          ForAll -> All+                          ExistsCh -> Exists in+              -- Use Logic.quant' here instead of the constructor+              -- Quantifier so as not to create quantifications with+              -- empty variable lists.+              q op' v (quant' op' vs f')+          Quantifier _ [] f' -> foldFirstOrder q c p f'+          Connective f1 Imply f2 -> c (BinOp f1 (:=>:) f2)+          Connective f1 Equiv f2 -> c (BinOp f1 (:<=>:) f2)+          Connective f1 And f2 -> c (BinOp f1 (:&:) f2)+          Connective f1 Or f2 -> c (BinOp f1 (:|:) f2)+          Predicate name ts -> p (L.Apply name ts)+          Equal t1 t2 -> p (L.Equal t1 t2)+    zipFirstOrder q c p f1 f2 =+        case (f1, f2) of+          (Not f1', Not f2') -> c ((:~:) f1') ((:~:) f2')+          (Quantifier op1 (v1:vs1) f1', Quantifier op2 (v2:vs2) f2') ->+              if op1 == op2+              then let op' = case op1 of+                               ForAll -> All+                               ExistsCh -> Exists in+                   q op' v1 (Quantifier op1 vs1 f1') All v2 (Quantifier op2 vs2 f2')+              else Nothing+          (Quantifier q1 [] f1', Quantifier q2 [] f2') ->+              if q1 == q2 then zipFirstOrder q c p f1' f2' else Nothing+          (Connective l1 op1 r1, Connective l2 op2 r2) ->+              case (op1, op2) of+                (And, And) -> c (BinOp l1 (:&:) r1) (BinOp l2 (:&:) r2)+                (Or, Or) -> c (BinOp l1 (:|:) r1) (BinOp l2 (:|:) r2)+                (Imply, Imply) -> c (BinOp l1 (:=>:) r1) (BinOp l2 (:=>:) r2)+                (Equiv, Equiv) -> c (BinOp l1 (:<=>:) r1) (BinOp l2 (:<=>:) r2)+                _ -> Nothing+          (Equal l1 r1, Equal l2 r2) -> p (L.Equal l1 r1) (L.Equal l2 r2)+          (Predicate p1 ts1, Predicate p2 ts2) -> p (L.Apply p1 ts1) (L.Apply p2 ts2)+          _ -> Nothing++instance (Ord v, Variable v, Data v, Eq f, Ord f, Skolem f, Data f) => Logic.Term (CTerm v f) v f where+    foldTerm v fn t =+        case t of+          Variable x -> v x+          Function f ts -> fn f ts+    zipT  v f t1 t2 =+        case (t1, t2) of+          (Variable v1, Variable v2) -> v v1 v2+          (Function f1 ts1, Function f2 ts2) -> f f1 ts1 f2 ts2+          _ -> Nothing+    var = Variable+    fApp f ts = Function f ts++data ConjunctiveNormalForm v p f =+    CNF [Sentence v p f]+    deriving (Eq)++data NormalSentence v p f+    = NFNot (NormalSentence v p f)+    | NFPredicate p [NormalTerm v f]+    | NFEqual (NormalTerm v f) (NormalTerm v f)+    deriving (Eq, Ord, Data, Typeable)++-- We need a distinct type here because of the functional dependencies+-- in class FirstOrderFormula.+data NormalTerm v f+    = NormalFunction f [NormalTerm v f]+    | NormalVariable v+    deriving (Eq, Ord, Data, Typeable)++instance Negatable (NormalSentence v p f) where+    (.~.) (NFNot (NFNot x)) = ((.~.) x)+    (.~.) (NFNot x)= x+    (.~.) x   = NFNot x+    negated (NFNot x) = not (negated x)+    negated _ = False++instance (Arity p, Boolean p, Logic (NormalSentence v p f)) => Pred p (NormalTerm v f) (NormalSentence v p f) where+    pApp0 x = NFPredicate x []+    pApp1 x a = NFPredicate x [a]+    pApp2 x a b = NFPredicate x [a,b]+    pApp3 x a b c = NFPredicate x [a,b,c]+    pApp4 x a b c d = NFPredicate x [a,b,c,d]+    pApp5 x a b c d e = NFPredicate x [a,b,c,d,e]+    pApp6 x a b c d e f = NFPredicate x [a,b,c,d,e,f]+    pApp7 x a b c d e f g = NFPredicate x [a,b,c,d,e,f,g]+    x .=. y = NFEqual x y+    x .!=. y = NFNot (NFEqual x y)++instance (Logic (NormalSentence v p f), Logic.Term (NormalTerm v f) v f,+          IsString v, Show v,+          Ord p, IsString p, Boolean p, Arity p, Data p, Show p,+          Ord f, IsString f, Show f) => FirstOrderFormula (NormalSentence v p f) (NormalTerm v f) v p f where+    for_all _ _ = error "FirstOrderFormula NormalSentence"+    exists _ _ = error "FirstOrderFormula NormalSentence"+    foldFirstOrder _ c p f =+        case f of+          NFNot x -> c ((:~:) x)+          NFEqual t1 t2 -> p (L.Equal t1 t2)+          NFPredicate pr ts -> p (L.Apply pr ts)+    zipFirstOrder _ c p f1 f2 =+        case (f1, f2) of+          (NFNot f1', NFNot f2') -> c ((:~:) f1') ((:~:) f2')+          (NFEqual f1l f1r, NFEqual f2l f2r) -> p (L.Equal f1l f1r) (L.Equal f2l f2r)+          (NFPredicate p1 ts1, NFPredicate p2 ts2) -> p (L.Apply p1 ts1) (L.Apply p2 ts2)+          _ -> Nothing++instance (Ord v, Variable v, Data v, Eq f, Ord f, Skolem f, Data f) => Logic.Term (NormalTerm v f) v f where+    var = NormalVariable+    fApp = NormalFunction+    foldTerm v f t =+            case t of+              NormalVariable x -> v x+              NormalFunction x ts -> f x ts+    zipT v fn t1 t2 =+        case (t1, t2) of+          (NormalVariable x1, NormalVariable x2) -> v x1 x2+          (NormalFunction f1 ts1, NormalFunction f2 ts2) -> fn f1 ts1 f2 ts2+          _ -> Nothing++toSentence :: FirstOrderFormula (Sentence v p f) (CTerm v f) v p f => NormalSentence v p f -> Sentence v p f+toSentence (NFNot s) = (.~.) (toSentence s)+toSentence (NFEqual t1 t2) = toTerm t1 .=. toTerm t2+toSentence (NFPredicate p ts) = pApp p (map toTerm ts)++toTerm :: (Ord v, Variable v, Data v, Eq f, Ord f, Skolem f, Data f) => NormalTerm v f -> CTerm v f+toTerm (NormalFunction f ts) = Logic.fApp f (map toTerm ts)+toTerm (NormalVariable v) = Logic.var v++fromSentence :: forall v p f. FirstOrderFormula (Sentence v p f) (CTerm v f) v p f =>+                Sentence v p f -> NormalSentence v p f+fromSentence = foldFirstOrder +                 (\ _ _ _ -> error "fromSentence 1")+                 (\ cm ->+                      case cm of+                        ((:~:) f) -> NFNot (fromSentence f)+                        _ -> error "fromSentence 2")+                 (\ pa ->+                      case pa of+                        L.Equal t1 t2 -> NFEqual (fromTerm t1) (fromTerm t2)+                        L.NotEqual t1 t2 -> NFNot (NFEqual (fromTerm t1) (fromTerm t2))+                        L.Constant x -> NFPredicate (fromBool x) []+                        L.Apply p ts -> NFPredicate p (map fromTerm ts))+++fromTerm :: CTerm v f -> NormalTerm v f+fromTerm (Function f ts) = NormalFunction f (map fromTerm ts)+fromTerm (Variable v) = NormalVariable v
+ Data/Logic/Instances/PropLogic.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -fno-warn-orphans #-}+module Data.Logic.Instances.PropLogic+    ( flatten+    , plSat0+    , plSat+    ) where++import Data.Logic.Classes.Boolean (Boolean(fromBool))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula, toPropositional)+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Propositional (PropositionalFormula(..), Combine(..), BinOp(..), clauseNormalForm')+import Data.Logic.Classes.Literal (Literal(..))+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (NormalT)+import qualified Data.Set.Extra as S+import PropLogic++instance Negatable (PropForm a) where+    (.~.) (N (N x)) = (.~.) x+    (.~.) (N x) = x+    (.~.) x = N x+    negated (N x) = not (negated x)+    negated _ = False++instance Ord a => Logic (PropForm a) where+    x .<=>. y = EJ [x, y]+    x .=>.  y = SJ [x, y]+    x .|.   y = DJ [x, y]+    x .&.   y = CJ [x, y]++instance (Logic (PropForm a), Ord a) => PropositionalFormula (PropForm a) a where+    atomic = A+    foldPropositional c a formula =+        case formula of+          -- EJ [x,y,z,...] -> CJ [EJ [x,y], EJ[y,z], ...]+          EJ [] -> error "Empty EJ"+          EJ [x] -> foldPropositional c a x+          EJ [x0, x1] -> c (BinOp x0 (:<=>:) x1)+          EJ xs -> foldPropositional c a (CJ (map (\ (x0, x1) -> EJ [x0, x1]) (pairs xs)))+          SJ [] -> error "Empty SJ"+          SJ [x] -> foldPropositional c a x+          SJ [x0, x1] -> c (BinOp x0 (:=>:) x1)+          SJ xs -> foldPropositional c a (CJ (map (\ (x0, x1) -> SJ [x0, x1]) (pairs xs)))+          DJ [] -> error "Empty disjunct"+          DJ [x] -> foldPropositional c a x+          DJ (x0:xs) -> c (BinOp x0 (:|:) (DJ xs))+          CJ [] -> error "Empty conjunct"+          CJ [x] -> foldPropositional c a x+          CJ (x0:xs) -> c (BinOp x0 (:&:) (CJ xs))+          N x -> c ((:~:) x)+          -- Not sure what to do about these - so far not an issue.+          T -> error "foldPropositional method of PropForm: T"+          F -> error "foldPropositional method of PropForm: F"+          A x -> a x++instance Boolean (PropForm formula) where+    fromBool True = T+    fromBool False = F++pairs :: [a] -> [(a, a)]+pairs (x:y:zs) = (x,y) : pairs (y:zs)+pairs _ = []++flatten :: PropForm a -> PropForm a+flatten (CJ xs) =+    CJ (concatMap f (map flatten xs))+    where+      f (CJ ys) = ys+      f x = [x]+flatten (DJ xs) =+    DJ (concatMap f (map flatten xs))+    where+      f (DJ ys) = ys+      f x = [x]+flatten (EJ xs) = EJ (map flatten xs)+flatten (SJ xs) = SJ (map flatten xs)+flatten (N x) = N (flatten x)+flatten x = x++plSat0 :: (PropAlg a (PropForm formula), PropositionalFormula formula atom) => PropForm formula -> Bool+plSat0 f = satisfiable . (\ (x :: PropForm formula) -> x) . clauses0 $ f++clauses0 :: PropositionalFormula formula atom => PropForm formula -> PropForm formula+clauses0 f = CJ . map DJ . map S.toList . S.toList $ clauseNormalForm' f++plSat :: forall m formula term v p f. (Monad m, FirstOrderFormula formula term v p f, Ord formula, Literal formula term v p f) =>+                formula -> NormalT v term m Bool+plSat f = clauses f >>= (\ (x :: PropForm formula) -> return x) >>= return . satisfiable++clauses :: forall m formula term v p f. (Monad m, FirstOrderFormula formula term v p f, Literal formula term v p f) =>+           formula -> NormalT v term m (PropForm formula)+clauses f = clauseNormalForm f >>= return . CJ . map (DJ . map (toPropositional (A :: formula -> PropForm formula))) . map S.toList . S.toList
+ Data/Logic/Instances/SatSolver.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables, StandaloneDeriving, TypeSynonymInstances #-}+{-# OPTIONS -fno-warn-orphans #-}+module Data.Logic.Instances.SatSolver where++import Control.Monad.State (get, put)+import Control.Monad.Trans (lift)+import Data.Boolean.SatSolver+import Data.Generics (Data, Typeable)+import qualified Data.Set.Extra as S+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))+import Data.Logic.Classes.ClauseNormalForm (ClauseNormalFormula(..))+import qualified Data.Logic.Classes.Literal as N+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (LiteralMapT, NormalT')+import qualified Data.Map as M++instance Ord Literal where+    compare (Neg _) (Pos _) = LT+    compare (Pos _) (Neg _) = GT+    compare (Pos m) (Pos n) = compare m n+    compare (Neg m) (Neg n) = compare m n++instance Negatable Literal where+    (.~.) (Pos n) = Neg n+    (.~.) (Neg n) = Pos n+    negated (Pos _) = False+    negated (Neg _) = True++deriving instance Data Literal+deriving instance Typeable Literal++instance ClauseNormalFormula CNF Literal where+    clauses = S.fromList . map S.fromList+    makeCNF = map S.toList . S.toList+    satisfiable cnf = return . not . null $ assertTrue' cnf newSatSolver >>= solve++toCNF :: (Monad m, FirstOrderFormula formula term v p f, N.Literal formula term v p f) =>+         formula -> NormalT' formula v term m CNF+toCNF f = clauseNormalForm f >>= S.ssMapM (lift . toLiteral) >>= return . makeCNF++-- |Convert a [[formula]] to CNF, which means building a map from+-- formula to Literal.+toLiteral :: forall m lit. (Monad m, Negatable lit, Ord lit) =>+             lit -> LiteralMapT lit m Literal+toLiteral f =+    literalNumber >>= return . if negated f then Neg else Pos+    where+      literalNumber :: LiteralMapT lit m Int+      literalNumber =+          get >>= \ (count, m) ->+          case M.lookup f' m of+            Nothing -> do let m' = M.insert f' count m+                          put (count+1, m') +                          return count+            Just n -> return n+      f' :: lit+      f' = if negated f then (.~.) f else f
+ Data/Logic/Instances/TPTP.hs view
@@ -0,0 +1,183 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,+             RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -fno-warn-missing-signatures -fno-warn-orphans #-}+module Logic.Instances.TPTP where++import Codec.TPTP (F(..), Formula, BinOp(..), V(..), T(..), Term0(..), AtomicWord(..), Formula0(..), InfixPred(..))+import qualified Codec.TPTP as TPTP+import Control.Monad.Identity (Identity(..))+import Data.Char (isDigit, ord)+import Data.Generics (Data, Typeable)+import Data.String (IsString(..))+import qualified Logic.FirstOrder as Logic+import Logic.FirstOrder (FirstOrderFormula(..), Term(..), Pretty(..), Predicate(..), Variable(next), pApp)+import qualified Logic.Logic as Logic+import Logic.Logic (Negatable(..), Logic(..), Boolean(..))+import qualified Logic.Propositional as Logic+import Text.PrettyPrint (text)++-- |Generate a series of variable names.+instance Variable V where+    one = V "VS1"+    next (V s) =+        V (case break (not . isDigit) (reverse s) of+             ("", "SV") -> "VS1"+             (digits, "SV") -> "VS" ++ show (1 + read (reverse digits) :: Int)+             _ -> "VS1")++instance Logic.Arity AtomicWord where+    arity _ = Nothing++instance Logic.Pretty V where+    pretty (V s) = text s++mn = 'x'+pref = 'x'+mx = 'z'+cnt = ord mx - ord mn + 1++-- |TPTP's Term type has two extra constructors that can be represented+-- using this augmented atomic function application type.+data AtomicFunction+    = Atom AtomicWord +    | StringLit String+    | NumberLit Double+    | Skolem V+    deriving (Eq, Ord, Show, Data, Typeable)++instance IsString AtomicFunction where+    fromString = Atom . AtomicWord++instance Logic.Skolem AtomicFunction where+    toSkolem = Skolem . V . ("sK" ++) . show+    fromSkolem (Skolem (V s)) = Just (read (drop 2 s) :: Int)+    fromSkolem _ = Nothing++-- |This is not a safe way to implement booleans.+instance Logic.Boolean AtomicWord where+    fromBool = AtomicWord . show++instance Logic.Pretty AtomicFunction where+    pretty (Atom w) = Logic.pretty w+    pretty (StringLit s) = text (show s)+    pretty (NumberLit n) = text (show n)+    pretty (Skolem (V s)) = text ("sK" ++ s)++instance Logic.Pretty AtomicWord where+    pretty (AtomicWord s) = text s++instance Logic.Negatable Formula where+    negated (F (Identity ((:~:) x))) = not (negated x)+    negated _ = False+    (.~.) (F (Identity ((:~:) x))) = x+    (.~.) x   = (.~.) x++-- |If this looks confusing, it is because TPTP has the same operators+-- as Logic, the .&. on the left is the Logic method name and .&. on+-- the right is the TPTP function.+instance Logic.Logic Formula where+    x .<=>. y = x .<=>. y+    x .=>.  y = x .=>. y+    x .<=.  y = x .<=. y+    x .|.   y = x .|. y+    x .&.   y = x .&. y+    x .<~>. y = x .<~>. y+    x .~|.  y = x .~|. y+    x .~&.  y = x .~&. y++-- |For types designed to represent first order (predicate) logic, it+-- is easiest to make the atomic type the same as the formula type,+-- and then raise an error if we see unexpected non-atomic formulas.+instance Logic.PropositionalFormula Formula Formula where+    atomic (F (Identity (InfixPred t1 (:=:) t2))) = t1 .=. t2+    atomic (F (Identity (InfixPred t1 (:!=:) t2))) = t1 .!=. t2+    atomic (F (Identity (PredApp p ts))) = pApp p ts+    atomic _ = error "atomic method of PropositionalFormula for TPTP: invalid argument"+    -- Use the TPTP fold to implement the Logic fold.  This means+    -- building wrappers around some of the functions so that when+    -- the wrappers are passed TPTP types they turn them into Logic+    -- values to pass to the argument functions.+    foldF0 c a form =+        TPTP.foldF n' q' b' i' p' (unwrapF' form)+        where q' = error "TPTP Formula with quantifier passed to foldF0"+              n' f = c ((Logic.:~:) f)+              b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2)+              b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1)+              b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2)+              b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2)+              -- The :~&: operator is not present in the Logic BinOp type,+              -- so we need to use the equivalent ~(a&b)+              b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2))+              b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2)+              b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2))+              b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2)))+              i' t1 (:=:) t2 = a (F (Identity (InfixPred t1 (:=:) t2)))+              i' t1 (:!=:) t2 = a (F (Identity (InfixPred t1 (:!=:) t2)))+              p' p ts = a (F (Identity (PredApp p ts)))+              unwrapF' (F x) = F x -- copoint x++instance Logic.FirstOrderFormula Formula (T Identity) V AtomicWord AtomicFunction where+    for_all vars x = for_all vars x+    exists vars x = exists vars x+    -- Use the TPTP fold to implement the Logic fold.  This means+    -- building wrappers around some of the functions so that when+    -- the wrappers are passed TPTP types they turn them into Logic+    -- values to pass to the argument functions.+    foldF q c p form =+        TPTP.foldF n' q' b' i' p' (unwrapF' form)+        where q' op (v:vs) form' =+                  let op' = case op of+                              TPTP.All -> Logic.All+                              TPTP.Exists -> Logic.Exists in+                  q op' v (foldr (\ v' f -> Logic.quant op' v' f) form' vs)+              q' _ [] form' = foldF q c p form'+              n' f = c ((Logic.:~:) f)+              b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2)+              b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1)+              b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2)+              b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2)+              -- The :~&: operator is not present in the Logic BinOp type,+              -- so we need to somehow use the equivalent ~(a&b)+              b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2))+              b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2)+              b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2))+              b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2)))+              i' t1 (:=:) t2 = p (Equal t1 t2)+              i' t1 (:!=:) t2 = p (NotEqual t1 t2) -- TPTP.foldF n' q' b' i' p' ((.~.) (t1 .=. t2))+              p' pr ts = p (Apply pr ts)+              unwrapF' (F x) = F x -- copoint x+    zipF = error "Unimplemented: Logic.Instances.TPTP.zipF"+    x .=. y   = x .=. y+    x .!=. y  = x .!=. y+    pApp0 p = TPTP.pApp p []+    pApp1 p a = TPTP.pApp p [a]+    pApp2 p a b = TPTP.pApp p [a,b]+    pApp3 p a b c = TPTP.pApp p [a,b,c]+    pApp4 p a b c d = TPTP.pApp p [a,b,c,d]+    pApp5 p a b c d e = TPTP.pApp p [a,b,c,d,e]+    pApp6 p a b c d e f = TPTP.pApp p [a,b,c,d,e,f]+    pApp7 p a b c d e f g = TPTP.pApp p [a,b,c,d,e,f,g]++instance (Eq AtomicFunction, Logic.Skolem AtomicFunction) => Logic.Term (T Identity) V AtomicFunction where+    foldT v fa term =+        -- We call the foldT function from the TPTP package here, which+        -- has a different signature from the foldT method we are+        -- implementing.  The two extra term types in TPTP are represented+        -- here as additional values in the AtomicFunction type.+        TPTP.foldT string double v atom (unwrapT' term)+        where atom w ts = fa (Atom w) ts+              string s = fa (StringLit s) []+              double n = fa (NumberLit n) []+              unwrapT' (T x) = T x -- copoint x+    zipT = error "Unimplemented: Logic.Instances.TPTP.zipT"+    var = var+    fApp x args = +        case x of+          Atom w -> TPTP.fApp w args+          StringLit s -> T {runT = Identity (DistinctObjectTerm s)}+          NumberLit n -> T {runT = Identity (NumberLitTerm n)}+          Skolem (V s) -> TPTP.fApp (AtomicWord ("Sk(" ++ s ++ ")")) args++--deriving instance Show TPTP.Term+--deriving instance (Show t, Show f) => Show (TPTP.Formula0 t f)+--deriving instance Show t => Show (TPTP.Term0 t)
+ Data/Logic/KnowledgeBase.hs view
@@ -0,0 +1,195 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes,+             TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall #-}++{- KnowledgeBase.hs -}+{- Charles Chiou, David Fox -}++module Data.Logic.KnowledgeBase+    ( WithId(WithId, wiItem, wiIdent) -- Probably only used by some unit tests, and not really correctly+    , ProverT+    , runProver'+    , runProverT'+    , getKB+    , unloadKB+    -- , deleteKB+    , askKB+    , theoremKB+    , inconsistantKB+    , ProofResult(Proved, Disproved, Invalid)+    , Proof(Proof, proofResult, proof)+    , validKB+    , tellKB+    , loadKB+    , showKB+    ) where++import Control.Monad.Identity (Identity(runIdentity))+import Control.Monad.State (StateT, evalStateT, MonadState(get, put))+import Control.Monad.Trans (lift)+import Data.Generics (Data, Typeable)+import Data.Logic.Classes.FirstOrder (FirstOrderFormula)+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Normal.Implicative (ImplicativeForm, implicativeNormalForm)+import Data.Logic.Normal.Skolem (NormalT, runNormalT)+import Data.Logic.Resolution (prove, SetOfSupport, getSetOfSupport)+import qualified Data.Set.Extra as S+import Prelude hiding (negate)++type SentenceCount = Int++data WithId a = WithId {wiItem :: a, wiIdent :: Int} deriving (Eq, Ord, Show, Data, Typeable)++withId :: Int -> a -> WithId a+withId i x = WithId {wiIdent = i, wiItem = x}++{-+withIdPairs :: [WithId a] -> [(a, Int)]+withIdPairs = map (\ x -> (wiItem x, wiIdent x))++wiLookupId :: Eq a => a -> [WithId a] -> Maybe Int+wiLookupId x xs = lookup x (withIdPairs xs)++withIdPairs' :: [WithId a] -> [(Int, a)]+withIdPairs' = map (\ x -> (wiIdent x, wiItem x))++wiLookupItem :: Int -> [WithId a] -> Maybe a+wiLookupItem i xs = lookup i (withIdPairs' xs)+-}++type KnowledgeBase inf = S.Set (WithId inf)++data ProverState inf+    = ProverState+      { knowledgeBase :: KnowledgeBase inf+      , sentenceCount :: Int }++zeroKB :: ProverState inf+zeroKB = ProverState+         { knowledgeBase = S.empty+         , sentenceCount = 1 }++-- |A monad for running the knowledge base.+type ProverT inf = StateT (ProverState inf)+type ProverT' v term inf m a = ProverT inf (NormalT v term m) a++runProverT' :: Monad m => ProverT' v term inf m a -> m a+runProverT' = runNormalT . runProverT+runProverT :: Monad m => StateT (ProverState inf) m a -> m a+runProverT action = evalStateT action zeroKB+runProver' :: ProverT' v term inf Identity a -> a+runProver' = runIdentity . runProverT'+{-+runProver :: StateT (ProverState inf) Identity a -> a+runProver = runIdentity . runProverT+-}++data ProofResult+    = Disproved+    -- ^ The conjecture is unsatisfiable+    | Proved+    -- ^ The negated conjecture is unsatisfiable+    | Invalid+    -- ^ Both are satisfiable+    deriving (Data, Typeable, Eq, Ord, Show)++data Proof lit = Proof {proofResult :: ProofResult, proof :: S.Set (ImplicativeForm lit)} deriving (Data, Typeable, Eq, Ord)++instance (Ord lit, Show lit, Literal lit term v p f, FirstOrderFormula lit term v p f) => Show (Proof lit) where+    show p = "Proof {proofResult = " ++ show (proofResult p) ++ ", proof = " ++ show (proof p) ++ "}"++-- |Remove a particular sentence from the knowledge base+unloadKB :: (Monad m, Ord inf) => SentenceCount -> ProverT inf m (Maybe (KnowledgeBase inf))+unloadKB n =+    do st <- get+       let (discard, keep) = S.partition ((== n) . wiIdent) (knowledgeBase st)+       put (st {knowledgeBase = keep}) >> return (Just discard)++-- |Return the contents of the knowledgebase.+getKB :: Monad m => ProverT inf m (S.Set (WithId inf))+getKB = get >>= return . knowledgeBase++-- |Return a flag indicating whether sentence was disproved, along+-- with a disproof.+inconsistantKB :: forall m formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>+                  formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)+inconsistantKB s = lift (implicativeNormalForm s) >>= return . getSetOfSupport >>= \ sos -> getKB >>= return . prove S.empty sos . S.map wiItem++-- |Return a flag indicating whether sentence was proved, along with a+-- proof.+theoremKB :: forall m formula term v p f lit. (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>+             formula -> ProverT' v term (ImplicativeForm lit) m (Bool, SetOfSupport lit v term)+theoremKB s = inconsistantKB ((.~.) s)++-- |Try to prove a sentence, return the result and the proof.+-- askKB should be in KnowledgeBase module. However, since resolution+-- is here functions are here, it is also placed in this module.+askKB :: (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>+         formula -> ProverT' v term (ImplicativeForm lit) m Bool+askKB s = theoremKB s >>= return . fst++-- |See whether the sentence is true, false or invalid.  Return proofs+-- for truth and falsity.+validKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>+           formula -> ProverT' v term (ImplicativeForm lit) m (ProofResult, SetOfSupport lit v term, SetOfSupport lit v term)+validKB s =+    theoremKB s >>= \ (proved, proof1) ->+    inconsistantKB s >>= \ (disproved, proof2) ->+    return (if proved then Proved else if disproved then Disproved else Invalid, proof1, proof2)++-- |Validate a sentence and insert it into the knowledgebase.  Returns+-- the INF sentences derived from the new sentence, or Nothing if the+-- new sentence is inconsistant with the current knowledgebase.+tellKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>+          formula -> ProverT' v term (ImplicativeForm lit) m (Proof lit)+tellKB s =+    do st <- get+       inf <- lift (implicativeNormalForm s)+       let inf' = S.map (withId (sentenceCount st)) inf+       (valid, _, _) <- validKB s+       case valid of+         Disproved -> return ()+         _ -> put st { knowledgeBase = S.union (knowledgeBase st) inf'+                     , sentenceCount = sentenceCount st + 1 }+       return $ Proof {proofResult = valid, proof = S.map wiItem inf'}++loadKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m) =>+          [formula] -> ProverT' v term (ImplicativeForm lit) m [Proof lit]+loadKB sentences = mapM tellKB sentences++-- |Delete an entry from the KB.+{-+deleteKB :: Monad m => Int -> ProverT inf m String+deleteKB i = do st <- get+                modify (\ st' -> st' {knowledgeBase = deleteElement i (knowledgeBase st')})+                st' <- get+		return (if length (knowledgeBase st') /= length (knowledgeBase st) then+			  "Deleted"+			else+			  "Failed to delete")+	     +deleteElement :: Int -> [a] -> [a]+deleteElement i l+    | i <= 0    = l+    | otherwise = let+		    (p1, p2) = splitAt (i - 1) l+		  in+		    p1 ++ (case p2 of+			       [] -> []+			       _ -> tail p2)+-}++-- |Return a text description of the contents of the knowledgebase.+showKB :: (Show inf, Monad m) => ProverT inf m String+showKB = get >>= return . reportKB++reportKB :: (Show inf) => ProverState inf -> String+reportKB st@(ProverState {knowledgeBase = kb}) =+    case S.minView kb of+      Nothing -> "Nothing in Knowledge Base\n"+      Just (WithId {wiItem = x, wiIdent = n}, kb')+          | S.null kb' ->+              show n ++ ") " ++ "\t" ++ show x ++ "\n"+          | True ->+              show n ++ ") " ++ "\t" ++ show x ++ "\n" ++ reportKB (st {knowledgeBase = kb'})
+ Data/Logic/Normal/Clause.hs view
@@ -0,0 +1,123 @@+-- |A series of transformations to convert first order logic formulas+-- into (ultimately) Clause Normal Form.+-- +-- @+-- 1st order formula:+--   ∀Y (∀X (taller(Y,X) | wise(X)) => wise(Y))+-- +-- Simplify+--   ∀Y (~∀X (taller(Y,X) | wise(X)) | wise(Y))+-- +-- Move negations in - Negation Normal Form+--   ∀Y (∃X (~taller(Y,X) & ~wise(X)) | wise(Y))+-- +-- Move quantifiers out - Prenex Normal Form+--   ∀Y (∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)))+-- +-- Distribute disjunctions+--   ∀Y ∃X ((~taller(Y,X) | wise(Y)) & (~wise(X) | wise(Y)))+-- +-- Skolemize  - Skolem Normal Form+--   ∀Y (~taller(Y,x(Y)) | wise(Y)) & (~wise(x(Y)) | wise(Y))+-- +-- Convert to CNF+--   { ~taller(Y,x(Y)) | wise(Y),+--     ~wise(x(Y)) | wise(Y) } +-- @+-- +{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wall #-}+module Data.Logic.Normal.Clause+    ( clauseNormalForm+    , trivial+    , cnfTrace+    ) where++import Data.Logic.Normal.Negation (negationNormalForm, nnf, simplify)+import Data.Logic.Normal.Prenex (prenexNormalForm)+import Data.Logic.Normal.Skolem (skolemNormalForm, NormalT)++import Data.List (intersperse)+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), prettyFirstOrder, Predicate(..))+import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Literal (Literal(..), prettyLit, fromFirstOrder)+import qualified Data.Set.Extra as Set+import Text.PrettyPrint (Doc, hcat, vcat, text, nest, ($$), brackets, render)++-- |Convert to Skolem Normal Form and then distribute the disjunctions over the conjunctions:+-- +-- @+-- Formula      Rewrites to+-- P | (Q & R)  (P | Q) & (P | R)+-- (Q & R) | P  (Q | P) & (R | P)+-- @+-- +clauseNormalForm :: (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>+       formula -> NormalT v term m (Set.Set (Set.Set lit))+clauseNormalForm fm = skolemNormalForm fm >>= return . simpcnf++cnfTrace :: forall m formula term v p f lit.+            (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f) =>+            (v -> Doc)+         -> (p -> Doc)+         -> (f -> Doc)+         -> formula+         -> NormalT v term m (String, Set.Set (Set.Set lit))+cnfTrace pv pp pf f =+    do let simplified = simplify f+           pnf = prenexNormalForm f+       snf <- skolemNormalForm f+       cnf <- clauseNormalForm f+       return (render (vcat+                       [text "Original:" $$ nest 2 (prettyFirstOrder pv pp pf 0 f),+                        text "Simplified:" $$ nest 2 (prettyFirstOrder pv pp pf 0 simplified),+                        text "Negation Normal Form:" $$ nest 2 (prettyFirstOrder pv pp pf 0 (negationNormalForm f)),+                        text "Prenex Normal Form:" $$ nest 2 (prettyFirstOrder pv pp pf 0 pnf),+                        text "Skolem Normal Form:" $$ nest 2 (prettyFirstOrder pv pp pf 0 snf),+                        text "Clause Normal Form:" $$ vcat (map prettyClause (fromSS cnf))]), cnf)+    where+      prettyClause (clause :: [lit]) =+          nest 2 . brackets . hcat . intersperse (text ", ") . map (nest 2 . brackets . prettyLit pv pp pf 0) $ clause+      fromSS = (map Set.toList) . Set.toList ++simpcnf :: forall formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f) =>+           formula -> Set.Set (Set.Set lit)+simpcnf fm =+    foldFirstOrder (\ _ _ _ -> cjs') (\ _ -> cjs') p fm+    where+      p (Apply pr _ts)+          | pr == fromBool False = Set.empty+          | pr == fromBool True = Set.singleton Set.empty+          | True = cjs'+      p (Equal _ _) = cjs'+      p (NotEqual _ _) = cjs'+      p (Constant _) = cjs'+      -- Discard any clause that is the proper subset of another clause+      cjs' = Set.filter keep cjs+      keep x = not (Set.or (Set.map (Set.isProperSubsetOf x) cjs))+      cjs = Set.filter (not . trivial) (purecnf (nnf fm)) :: Set.Set (Set.Set lit)++-- |Harrison page 59.  Look for complementary pairs in a clause.+trivial :: (Negatable lit, Ord lit) => Set.Set lit -> Bool+trivial lits =+    not . Set.null $ Set.intersection (Set.map (.~.) n) p+    where (n, p) = Set.partition negated lits++-- | CNF: (a | b | c) & (d | e | f)+purecnf :: forall formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f) =>+           formula -> Set.Set (Set.Set lit)+purecnf fm = Set.map (Set.map (.~.)) (purednf (nnf ((.~.) fm)))++purednf :: forall formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f) =>+           formula -> Set.Set (Set.Set lit)+purednf fm =+    foldFirstOrder (\ _ _ _ -> x) c (\ _ -> x)  fm+    where+      c :: Combine formula -> Set.Set (Set.Set lit)+      c (BinOp p (:&:) q) = Set.distrib (purednf p) (purednf q)+      c (BinOp p (:|:) q) = Set.union (purednf p) (purednf q)+      c _ = x+      x :: Set.Set (Set.Set lit)+      x = Set.singleton (Set.singleton (fromFirstOrder id id id fm)) :: Set.Set (Set.Set lit)
+ Data/Logic/Normal/Implicative.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wall #-}+module Data.Logic.Normal.Implicative+    ( ImplicativeForm(INF, neg, pos)+    , makeINF'+    , implicativeNormalForm+    , prettyINF+    , prettyProof+    ) where++import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (NormalT)++import Control.Monad.State (MonadPlus, msum)+import Data.Generics (Data, Typeable, listify)+import Data.List (intersperse)+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))+import Data.Logic.Classes.Skolem (Skolem(fromSkolem))+import Data.Logic.Classes.Literal (Literal(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import qualified Data.Set.Extra as Set+import Data.Maybe (isJust)+import Text.PrettyPrint (Doc, cat, text, hsep)++-- |A type to represent a formula in Implicative Normal Form.  Such a+-- formula has the form @a & b & c .=>. d | e | f@, where a thru f are+-- literals.  One more restriction that is not implied by the type is+-- that no literal can appear in both the pos set and the neg set.+data (Negatable lit, Ord lit) => ImplicativeForm lit =+    INF {neg :: Set.Set lit, pos :: Set.Set lit}+    deriving (Eq, Ord, Data, Typeable, Show)++-- |A version of MakeINF that takes lists instead of sets, used for+-- implementing a more attractive show method.+makeINF' :: (Negatable lit, Ord lit) => [lit] -> [lit] -> ImplicativeForm lit+makeINF' n p = INF (Set.fromList n) (Set.fromList p)++prettyINF :: (Negatable lit, Ord lit) => (lit -> Doc) -> ImplicativeForm lit -> Doc+prettyINF lit x = cat $ [text "(", hsep (map lit (Set.toList (neg x))),+                         text ") => (", hsep (map lit (Set.toList (pos x))), text ")"]++prettyProof :: (Negatable lit, Ord lit) => (lit -> Doc) -> Set.Set (ImplicativeForm lit) -> Doc+prettyProof lit p = cat $ [text "["] ++ intersperse (text ", ") (map (prettyINF lit) (Set.toList p)) ++ [text "]"]++-- |Take the clause normal form, and turn it into implicative form,+-- where each clauses becomes an (LHS, RHS) pair with the negated+-- literals on the LHS and the non-negated literals on the RHS:+-- @+--   (a | ~b | c | ~d) becomes (b & d) => (a | c)+--   (~b | ~d) | (a | c)+--   ~~(~b | ~d) | (a | c)+--   ~(b & d) | (a | c)+-- @+-- If there are skolem functions on the RHS, split the formula using+-- this identity:+-- @+--   (a | b | c) => (d & e & f)+-- @+-- becomes+-- @+--    a | b | c => d+--    a | b | c => e+--    a | b | c => f+-- @+implicativeNormalForm :: forall m formula term v p f lit. +                         (Monad m, FirstOrderFormula formula term v p f, Data formula, Literal lit term v p f) =>+                         formula -> NormalT v term m (Set.Set (ImplicativeForm lit))+implicativeNormalForm formula =+    do cnf <- clauseNormalForm formula+       let pairs = Set.map (Set.fold collect (Set.empty, Set.empty)) cnf :: Set.Set (Set.Set lit, Set.Set lit)+           pairs' = Set.flatten (Set.map split pairs) :: Set.Set (Set.Set lit, Set.Set lit)+       return (Set.map (\ (n,p) -> INF n p) pairs')+    -- clauseNormalForm formula >>= return . Set.unions . Set.map split . map (Set.fold collect (Set.empty, Set.empty))+    where+      collect :: lit -> (Set.Set lit, Set.Set lit) -> (Set.Set lit, Set.Set lit)+      collect f (n, p) =+          foldLiteral (\ f' -> (Set.insert f' n, p))+                      (\ _ -> (n, Set.insert f p))+                      f+      split :: (Set.Set lit, Set.Set lit) -> Set.Set (Set.Set lit, Set.Set lit)+      split (lhs, rhs) =+          if any isJust (map fromSkolem (gFind rhs :: [f]))+          then Set.map (\ x -> (lhs, Set.singleton x)) rhs+          else Set.singleton (lhs, rhs)++-- | @gFind a@ will extract any elements of type @b@ from+-- @a@'s structure in accordance with the MonadPlus+-- instance, e.g. Maybe Foo will return the first Foo+-- found while [Foo] will return the list of Foos found.+gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b+gFind = msum . map return . listify (const True)
+ Data/Logic/Normal/Negation.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wall #-}+module Data.Logic.Normal.Negation+    ( negationNormalForm+    , nnf+    , simplify+    ) where++import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), freeVars, quant, Quant(..), Predicate(..))+import Data.Logic.Classes.Propositional (Combine(..), combine, BinOp(..))+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Logic (Logic(..))+import qualified Data.Set.Extra as S++-- | Simplify and recursively apply nnf.+negationNormalForm :: FirstOrderFormula formula term v p f => formula -> formula+negationNormalForm = nnf . simplify++-- |Eliminate => and <=> and move negations inwards:+-- +-- @+-- Formula      Rewrites to+--  P => Q      ~P | Q+--  P <=> Q     (P & Q) | (~P & ~Q)+-- ~∀X P        ∃X ~P+-- ~∃X P        ∀X ~P+-- ~(P & Q)     (~P | ~Q)+-- ~(P | Q)     (~P & ~Q)+-- ~~P  P+-- @+-- +nnf :: FirstOrderFormula formula term v p f => formula -> formula+nnf fm =+    foldFirstOrder nnfQuant nnfCombine (\ _ -> fm) fm+    where+      nnfQuant op v p = quant op v (nnf p)+      nnfCombine ((:~:) p) = foldFirstOrder nnfNotQuant nnfNotCombine (\ _ -> fm) p+      nnfCombine (BinOp p (:=>:) q) = nnf ((.~.) p) .|. (nnf q)+      nnfCombine (BinOp p (:<=>:) q) =  (nnf p .&. nnf q) .|. (nnf ((.~.) p) .&. nnf ((.~.) q))+      nnfCombine (BinOp p (:&:) q) = nnf p .&. nnf q+      nnfCombine (BinOp p (:|:) q) = nnf p .|. nnf q+      nnfNotQuant All v p = exists v (nnf ((.~.) p))+      nnfNotQuant Exists v p = for_all v (nnf ((.~.) p))+      nnfNotCombine ((:~:) p) = nnf p+      nnfNotCombine (BinOp p (:&:) q) = nnf ((.~.) p) .|. nnf ((.~.) q)+      nnfNotCombine (BinOp p (:|:) q) = nnf ((.~.) p) .&. nnf ((.~.) q)+      nnfNotCombine (BinOp p (:=>:) q) = nnf p .&. nnf ((.~.) q)+      nnfNotCombine (BinOp p (:<=>:) q) = (nnf p .&. nnf ((.~.) q)) .|. nnf ((.~.) p) .&. nnf q++-- |Do a bottom-up recursion to simplify a formula.+simplify :: FirstOrderFormula formula term v p f => formula -> formula+simplify fm =+    foldFirstOrder (\ op v p -> simplify1 (quant op v (simplify p)))+          (\ cm -> case cm of+                     (:~:) p -> simplify1 ((.~.) (simplify p))+                     BinOp p op q -> simplify1 (combine (BinOp (simplify p) op (simplify q))))+          (\ _ -> simplify1 fm)+          fm++-- |Extend psimplify1 to handle quantifiers.  Any quantifier which has+-- no corresponding free occurrences of the quantified variable is+-- eliminated.+simplify1 :: FirstOrderFormula formula term v p f => formula -> formula+simplify1 fm =+    foldFirstOrder (\ _ v p -> if S.member v (freeVars p) then fm else p)+          (\ _ -> psimplify1 fm)+          (\ _ -> psimplify1 fm)+          fm++-- |Do one step of simplify for propositional formulas:+-- Perform the following transformations everywhere, plus any+-- commuted versions for &, |, and <=>.+-- +-- @+--  ~False      -> True+--  ~True       -> False+--  True & P    -> P+--  False & P   -> False+--  True | P    -> True+--  False | P   -> P+--  True => P   -> P+--  False => P  -> True+--  P => True   -> P+--  P => False  -> True+--  True <=> P  -> P+--  False <=> P -> ~P+-- @+-- +psimplify1 :: forall formula term v p f. FirstOrderFormula formula term v p f => formula -> formula+psimplify1 fm =+    foldFirstOrder (\ _ _ _ -> fm) simplifyCombine (\ _ -> fm) fm+    where+      simplifyCombine ((:~:) f) = foldFirstOrder (\ _ _ _ -> fm) simplifyNotCombine simplifyNotPred f+      simplifyCombine (BinOp l op r) =+          case (pBool l, op, pBool r) of+            (Just True,  (:&:), _)            -> r+            (Just False, (:&:), _)            -> false+            (_,          (:&:), Just True)    -> l+            (_,          (:&:), Just False)   -> false+            (Just True,  (:|:), _)            -> true+            (Just False, (:|:), _)            -> r+            (_,          (:|:), Just True)    -> true+            (_,          (:|:), Just False)   -> l+            (Just True,  (:=>:), _)           -> r+            (Just False, (:=>:), _)           -> true+            (_,          (:=>:), Just True)   -> true+            (_,          (:=>:), Just False)  -> (.~.) l+            (Just True,  (:<=>:), _)          -> r+            (Just False, (:<=>:), _)          -> (.~.) r+            (_,          (:<=>:), Just True)  -> l+            (_,          (:<=>:), Just False) -> (.~.) l+            _                                 -> fm+      simplifyNotCombine ((:~:) f) = f+      simplifyNotCombine _ = fm+      simplifyNotPred (Apply pr ts)+          | pr == fromBool False = pApp0 (fromBool True)+          | pr == fromBool True = pApp0 (fromBool False)+          | True = (.~.) (pApp pr ts)+      simplifyNotPred (Constant x) = pApp0 (fromBool (not x))+      simplifyNotPred (Equal t1 t2) = t1 .!=. t2+      simplifyNotPred (NotEqual t1 t2) = t1 .=. t2+      -- Return a Maybe Bool depending upon whether a formula is true,+      -- false, or something else.+      pBool :: formula -> Maybe Bool+      pBool = foldFirstOrder (\ _ _ _ -> Nothing) (\ _ -> Nothing) p+          where p (Apply pr _ts) =+                    if pr == fromBool True+                    then Just True+                    else if pr == fromBool False+                         then Just False+                         else Nothing+                p _ = Nothing
+ Data/Logic/Normal/Prenex.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wall #-}+module Data.Logic.Normal.Prenex+    ( prenexNormalForm+    ) where++import Data.Logic.Normal.Negation (negationNormalForm)++import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), freeVars, quant, Quant(..), substitute)+import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Term (Term(var))+import Data.Logic.Classes.Variable (variant)++-- |Convert to Prenex normal form, with all quantifiers at the left.+prenexNormalForm :: (FirstOrderFormula formula term v p f) => formula -> formula+prenexNormalForm = prenex . negationNormalForm++-- |Recursivly apply pullQuants anywhere a quantifier might not be+-- leftmost.+prenex :: (FirstOrderFormula formula term v p f) => formula -> formula +prenex fm =+    foldFirstOrder q c (\ _ -> fm) fm+    where+      q op x p = quant op x (prenex p)+      c (BinOp l (:&:) r) = pullQuants (prenex l .&. prenex r)+      c (BinOp l (:|:) r) = pullQuants (prenex l .|. prenex r)+      c _ = fm++-- |Perform transformations to move quantifiers outside of binary+-- operators:+-- +-- @+--  Formula            Rewrites to+--  (1) ∀x F[x] & G        ∀x    (F[x] & G)+--  (2) ∀x F[x] & ∀x G[x]  ∀x ∀x (F[x] & G[x])+--  (3) ∃x F[x] & G        ∃x    (F[x] & G)+--  (4) ∃x F[x] & ∃x G[x]  ∃x Yz (F[x] & G[z]) -- rename+-- +--  (5) ∀x F[x] | G        ∀x    (F[x] | G)+--  (6) ∀x F[x] | ∀x G[x]  ∀x ∀z (F[x] | G[z]) -- rename+--  (7) ∃x F[x] | G        ∃x    (F[x] | G)+--  (8) ∃x F[x] | ∃x G[x]  ∃x Yx (F[x] | G[x])+-- @+pullQuants :: forall formula term v p f. (FirstOrderFormula formula term v p f) => formula -> formula+pullQuants fm =+    foldFirstOrder (\ _ _ _ -> fm) pullQuantsCombine (\ _ -> fm) fm+    where+      getQuant = foldFirstOrder (\ op v f -> Just (op, v, f)) (\ _ -> Nothing) (\ _ -> Nothing)+      pullQuantsCombine ((:~:) _) = fm+      pullQuantsCombine (BinOp l op r) = +          case (getQuant l, op, getQuant r) of+            (Just (All, vl, l'),    (:&:), Just (All, vr, r'))    -> pullq True  True  fm for_all (.&.) vl vr l' r'+            (Just (Exists, vl, l'), (:|:), Just (Exists, vr, r')) -> pullq True  True  fm exists  (.|.) vl vr l' r'+            (Just (All, vl, l'),    (:&:), _)                     -> pullq True  False fm for_all (.&.) vl vl l' r+            (_,                     (:&:), Just (All, vr, r'))    -> pullq False True  fm for_all (.&.) vr vr l  r'+            (Just (All, vl, l'),    (:|:), _)                     -> pullq True  False fm for_all (.|.) vl vl l' r+            (_,                     (:|:), Just (All, vr, r'))    -> pullq False True  fm for_all (.|.) vr vr l  r'+            (Just (Exists, vl, l'), (:&:), _)                     -> pullq True  False fm exists  (.&.) vl vl l' r+            (_,                     (:&:), Just (Exists, vr, r')) -> pullq False True  fm exists  (.&.) vr vr l  r'+            (Just (Exists, vl, l'), (:|:), _)                     -> pullq True  False fm exists  (.|.) vl vl l' r+            (_,                     (:|:), Just (Exists, vr, r')) -> pullq False True  fm exists  (.|.) vr vr l  r'+            _                                                     -> fm++-- |Helper function to rename variables when we want to enclose a+-- formula containing a free occurrence of that variable a quantifier+-- that quantifies it.+pullq :: FirstOrderFormula formula term v p f =>+         Bool -> Bool -> formula -> (v -> formula -> formula) -> (formula -> formula -> formula) -> v -> v -> formula -> formula -> formula+pullq l r fm mkq op x y p q =+    let z = variant (freeVars fm) x+        p' = if l then substitute x (var z) p else p+        q' = if r then substitute y (var z) q else q+        fm' = pullQuants (op p' q') in+    mkq z fm'
+ Data/Logic/Normal/Skolem.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# OPTIONS -Wall #-}+module Data.Logic.Normal.Skolem+    ( LiteralMapT+    , NormalT+    , runNormalT+    , runNormal+    , NormalT'+    , runNormalT'+    , runNormal'+    , skolemNormalForm+    ) where++import Data.Logic.Normal.Negation (negationNormalForm)+import Data.Logic.Normal.Prenex (prenexNormalForm)++import Control.Monad.Identity (Identity(runIdentity))+import Control.Monad.State (StateT(runStateT), get, put)+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), freeVars, Quant(..), substitute)+import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Term (Term(var, fApp))+import Data.Logic.Classes.Skolem (Skolem(toSkolem))+import qualified Data.Map as Map+import qualified Data.Set as Set+ +--type LiteralMap f = LiteralMapT f Identity+type LiteralMapT f = StateT (Int, Map.Map f Int)++--runLiteralMap :: LiteralMap p a -> a+--runLiteralMap action = runIdentity (runLiteralMapM action)++runLiteralMapM :: Monad m => LiteralMapT f m a -> m a+runLiteralMapM action = (runStateT action) (1, Map.empty) >>= return . fst++-- |The logic monad contains (will contain) several types of state to+-- support the operations done on logic formulas: Skolemization,+-- literal substitution, and the set of support during a proof+-- procedure.+data LogicState v term+    = LogicState+      { skolemCount :: Int+        -- ^ The next available Skolem number.+      , skolemMap :: Map.Map v term+        -- ^ Map from variables to applications of a Skolem function+      , univQuant :: [v]+        -- ^ The variables which are universally quantified in the+        -- current scope, in the order they were encountered.  During+        -- Skolemization these are the parameters passed to the Skolem+        -- function.+      }++newLogicState :: LogicState v term+newLogicState = LogicState { skolemCount = 1+                           , skolemMap = Map.empty+                           , univQuant = [] }++type NormalT v term m = StateT (LogicState v term) m++runNormalT :: Monad m => NormalT v term m a -> m a+runNormalT action = (runStateT action) newLogicState >>= return . fst++runNormal :: NormalT v term Identity a -> a+runNormal = runIdentity . runNormalT++-- |Combination of Normal monad and LiteralMap monad+type NormalT' formula v term m a = NormalT v term (LiteralMapT formula m) a++runNormalT' :: Monad m => NormalT' formula v term m a -> m a+runNormalT' action = runLiteralMapM (runNormalT action)++runNormal' :: NormalT' formula v term Identity a -> a+runNormal' = runIdentity . runNormalT'++-- |We get Skolem Normal Form by skolemizing and then converting to+-- Prenex Normal Form, and finally eliminating the remaining quantifiers.+skolemNormalForm :: (Monad m, FirstOrderFormula formula term v p f) => formula -> NormalT v term m formula+skolemNormalForm f = askolemize f >>= return . specialize . prenexNormalForm++-- |I need to consult the Harrison book for the reasons why we don't+-- |just Skolemize the result of prenexNormalForm.+askolemize :: (Monad m, FirstOrderFormula formula term v p f) => formula -> NormalT v term m formula+askolemize = skolem . negationNormalForm {- nnf . simplify -}++-- |Skolemize the formula by removing the existential quantifiers and+-- replacing the variables they quantify with skolem functions (and+-- constants, which are functions of zero variables.)  The Skolem+-- functions are new functions (obtained from the NormalT monad) which+-- are applied to the list of variables which are universally+-- quantified in the context where the existential quantifier+-- appeared.+skolem :: (Monad m, FirstOrderFormula formula term v p f) => formula -> NormalT v term m formula+skolem fm =+    foldFirstOrder q c (\ _ -> return fm) fm+    where+      q Exists y p =+          do let xs = freeVars fm+             state <- get+             let f = toSkolem (skolemCount state)+             put (state {skolemCount = skolemCount state + 1})+             let fx = fApp f (map var (Set.toList xs))+             skolem (substitute y fx p)+      q All x p = skolem p >>= return . for_all x+      c (BinOp l (:&:) r) = skolem2 (.&.) l r+      c (BinOp l (:|:) r) = skolem2 (.|.) l r+      c _ = return fm++skolem2 :: (Monad m, FirstOrderFormula formula term v p f) =>+           (formula -> formula -> formula) -> formula -> formula -> NormalT v term m formula+skolem2 cons p q =+    skolem p >>= \ p' ->+    skolem q >>= \ q' ->+    return (cons p' q')++specialize :: FirstOrderFormula formula term v p f => formula -> formula+specialize f =+    foldFirstOrder q (\ _ -> f) (\ _ -> f) f+    where+      q All _ f' = specialize f'+      q _ _ _ = f
+ Data/Logic/Resolution.hs view
@@ -0,0 +1,350 @@+{-# LANGUAGE FlexibleContexts, RankNTypes, ScopedTypeVariables, TypeFamilies #-}+{-# OPTIONS -Wall -Wwarn #-}++{- Resolution.hs -}+{- Charles Chiou, David Fox -}++module Data.Logic.Resolution+    ( prove+    , getSetOfSupport+    , SetOfSupport+    , Unification+    , Subst )+    where++import Data.Logic.Classes.Term (Term(..))+import Data.Logic.Classes.Literal (Literal(..), PredicateLit(..))+import Data.Logic.Normal.Implicative (ImplicativeForm(INF, neg, pos))+import qualified Data.Set.Extra as S+import Data.Map (Map, empty)+import qualified Data.Map as M+import Data.Maybe (isJust)++type Subst v term = Map v term++type SetOfSupport lit v term = S.Set (Unification lit v term)++type Unification lit v term = (ImplicativeForm lit, Subst v term)++prove :: Literal lit term v p f =>+         SetOfSupport lit v term -> SetOfSupport lit v term -> S.Set (ImplicativeForm lit) -> (Bool, SetOfSupport lit v term)+prove ss1 ss2' kb =+    case S.minView ss2' of+      Nothing -> (False, ss1)+      Just (s, ss2) ->+          case prove' s kb ss2 ss1 of+            (ss', True) -> (True, (S.insert s (S.union ss1 ss')))+            (ss', False) -> prove (S.insert s ss1) ss' (S.insert (fst s) kb)+-- prove ss1 [] _kb = (False, ss1)+-- prove ss1 (s:ss2) kb =+--     let+--       (ss', tf) = prove' s kb ss2 ss1+--     in+--       if tf then+--         (True, (ss1 ++ [s] ++ss'))+--       else+--         prove (ss1 ++ [s]) ss' (fst s:kb)+prove' :: forall lit p f v term.+          Literal lit term v p f =>+          Unification lit v term -> S.Set (ImplicativeForm lit) -> SetOfSupport lit v term -> SetOfSupport lit v term -> (SetOfSupport lit v term, Bool)+prove' p kb ss1 ss2 =+    let+      res1 = S.map (\x -> resolution p (x, empty)) kb+      res2 = S.map (\x -> resolution (x, empty) p) kb+      dem1 = S.map (\e -> demodulate p (e, empty)) kb+      dem2 = S.map (\p' -> demodulate (p', empty) p) kb+      (ss', tf) = getResult (S.union ss1 ss2) (S.unions [res1, res2, dem1, dem2])+    in+      if S.null ss' then (ss1, False) else (S.union ss1 ss', tf)++getResult :: Literal lit term v p f =>+             (SetOfSupport lit v term) -> S.Set (Maybe (Unification lit v term)) -> ((SetOfSupport lit v term), Bool)+getResult ss us =+    case S.minView us of+      Nothing ->+          (S.empty, False)+      Just (Nothing, xs) ->+          getResult ss xs+      Just ((Just x@(inf, _v)), xs) ->+          if S.null (neg inf) && S.null (pos inf)+          then (S.singleton x, True)+          else if S.any id (S.map (\(e,_) -> isRenameOf (fst x) e) ss)+               then getResult ss xs+               else let (xs', tf) = getResult ss xs in (S.insert x xs', tf)+{-+getResult _ [] = (S.empty, False)+getResult ss (Nothing:xs) = getResult ss xs+getResult ss ((Just x):xs)  =+    if S.null (neg inf) && S.null (pos inf)+    then (S.singleton x, True)+    else if S.any id (S.map (\(e,_) -> isRenameOf (fst x) e) ss)+         then getResult ss xs+         else let (xs', tf) = getResult ss xs in (S.insert x xs' tf)+    where+      (inf, _v) = x+-}++-- |Convert the "question" to a set of support.+getSetOfSupport :: (Literal formula term v p f) =>+                   S.Set (ImplicativeForm formula) -> S.Set (ImplicativeForm formula, Subst v term)+getSetOfSupport s = S.map (\ x -> (x, getSubsts x empty)) s++getSubsts :: (Literal formula term v p f) =>+             ImplicativeForm formula -> Subst v term -> Subst v term+getSubsts inf theta =+    getSubstSentences (pos inf) (getSubstSentences (neg inf) theta)++getSubstSentences :: Literal formula term v p f => S.Set formula -> Subst v term -> Subst v term+getSubstSentences xs theta = foldr getSubstSentence theta (S.toList xs)+++getSubstSentence :: Literal formula term v p f => formula -> Subst v term -> Subst v term+getSubstSentence formula theta =+    foldLiteral+          (\ s -> getSubstSentence s theta)+          (\ pa -> case pa of+                     EqualLit t1 t2 -> getSubstsTerms [t1, t2] theta+                     ApplyLit _ ts -> getSubstsTerms ts theta)+          formula++getSubstsTerms :: Term term v f => [term] -> Subst v term -> Subst v term+getSubstsTerms [] theta = theta+getSubstsTerms (x:xs) theta =+    let+      theta' = getSubstsTerm x theta+      theta'' = getSubstsTerms xs theta'+    in+      theta''++getSubstsTerm :: Term term v f => term -> Subst v term -> Subst v term+getSubstsTerm term theta =+    foldTerm (\ v -> M.insertWith (\ _ old -> old) v (var v) theta)+             (\ _ ts -> getSubstsTerms ts theta)+             term++isRenameOf :: Literal lit term v p f =>+              ImplicativeForm lit -> ImplicativeForm lit -> Bool+isRenameOf inf1 inf2 =+    (isRenameOfSentences lhs1 lhs2) && (isRenameOfSentences rhs1 rhs2)+    where+      lhs1 = neg inf1+      rhs1 = pos inf1+      lhs2 = neg inf2+      rhs2 = pos inf2++isRenameOfSentences :: Literal lit term v p f => S.Set lit -> S.Set lit -> Bool+isRenameOfSentences xs1 xs2 =+    S.size xs1 == S.size xs2 && all (uncurry isRenameOfSentence) (zip (S.toList xs1) (S.toList xs2))++isRenameOfSentence :: forall formula term v p f. Literal formula term v p f => formula -> formula -> Bool+isRenameOfSentence f1 f2 =+    maybe False id $+    zipLiterals (\ _ _ -> Just False) p f1 f2+    where p :: PredicateLit p term -> PredicateLit p term -> Maybe Bool+          p (EqualLit t1l t1r) (EqualLit t2l t2r) = Just (isRenameOfTerm t1l t2l && isRenameOfTerm t1r t2r)+          p (ApplyLit p1 ts1) (ApplyLit p2 ts2) = Just (p1 == p2 && isRenameOfTerms ts1 ts2)+          p _ _ = Nothing++isRenameOfTerm :: Term term v f => term -> term -> Bool+isRenameOfTerm t1 t2 =+    maybe False id $+    zipT (\ _ _ -> Just True)+         (\ f1 ts1 f2 ts2 -> Just (f1 == f2 && isRenameOfTerms ts1 ts2))+         t1 t2++isRenameOfTerms :: Term term v f => [term] -> [term] -> Bool+isRenameOfTerms ts1 ts2 =+    if length ts1 == length ts2 then+      let+        tsTuples = zip ts1 ts2+      in+        foldl (&&) True (map (\(t1, t2) -> isRenameOfTerm t1 t2) tsTuples)+    else+      False++resolution :: forall lit p f term v. Literal lit term v p f =>+             (ImplicativeForm lit, Subst v term) -> (ImplicativeForm lit, Subst v term) -> Maybe (ImplicativeForm lit, Map v term)+resolution (inf1, theta1) (inf2, theta2) =+    let+        lhs1 = neg inf1+        rhs1 = pos inf1+        lhs2 = neg inf2+        rhs2 = pos inf2+        unifyResult = tryUnify rhs1 lhs2+    in+      case unifyResult of+        Just ((rhs1', theta1'), (lhs2', theta2')) ->+            let+              lhs'' = S.union (S.catMaybes $ S.map (\s -> subst s theta1') lhs1)+                              (S.catMaybes $ S.map (\s -> subst s theta2') lhs2')+              rhs'' = S.union (S.catMaybes $ S.map (\s -> subst s theta1') rhs1')+                              (S.catMaybes $ S.map (\s -> subst s theta2') rhs2)+              theta = M.unionWith (\ l _r -> l) (updateSubst theta1 theta1') (updateSubst theta2 theta2')+            in+              Just (INF lhs'' rhs'', theta)+        Nothing -> Nothing+    where+      tryUnify :: (Literal formula term v p f, Ord formula) =>+                  S.Set formula -> S.Set formula -> Maybe ((S.Set formula, Subst v term), (S.Set formula, Subst v term))+      tryUnify lhs rhs = tryUnify' lhs rhs S.empty+                         +      tryUnify' :: (Literal formula term v p f, Ord formula) =>+                   S.Set formula -> S.Set formula -> S.Set formula -> Maybe ((S.Set formula, Subst v term), (S.Set formula, Subst v term))+      tryUnify' lhss _ _ | S.null lhss = Nothing+      tryUnify' lhss'' rhss lhss' =+          let (lhs, lhss) = S.deleteFindMin lhss'' in+          case tryUnify'' lhs rhss S.empty of+            Nothing -> tryUnify' lhss rhss (S.insert lhs lhss')+            Just (rhss', theta1', theta2') ->+                Just ((S.union lhss' lhss, theta1'), (rhss', theta2'))++      tryUnify'' :: (Literal formula term v p f, Ord formula) =>+                    formula -> S.Set formula -> S.Set formula -> Maybe (S.Set formula, Subst v term, Subst v term)+      tryUnify'' _x rhss _ | S.null rhss = Nothing+      tryUnify'' x rhss'' rhss' =+          let (rhs, rhss) = S.deleteFindMin rhss'' in+          case unify x rhs of+            Nothing -> tryUnify'' x rhss (S.insert rhs rhss')+            Just (theta1', theta2') -> Just (S.union rhss' rhss, theta1', theta2')++-- |Try to unify the second argument using the equality in the first.+demodulate :: (Literal lit term v p f) =>+              (Unification lit v term) -> (Unification lit v term) -> Maybe (Unification lit v term)+demodulate (inf1, theta1) (inf2, theta2) =+    case (S.null (neg inf1), S.toList (pos inf1)) of+      (True, [lit1]) ->+          foldLiteral (\ _ -> error "demodulate") p lit1+      _ -> Nothing+    where+      p (EqualLit t1 t2) =+          case findUnify t1 t2 (S.union lhs2 rhs2) of+            Just ((t1', t2'), theta1', theta2') ->+                let substNeg2 = S.catMaybes $ S.map (\x -> subst x theta2') lhs2+                    substPos2 = S.catMaybes $ S.map (\x -> subst x theta2') rhs2+                    lhs = S.catMaybes $ S.map (\x -> replaceTerm x (t1', t2')) substNeg2+                    rhs = S.catMaybes $ S.map (\x -> replaceTerm x (t1', t2')) substPos2+                    theta = M.unionWith (\ l _r -> l) (updateSubst theta1 theta1') (updateSubst theta2 theta2') in+                Just (INF lhs rhs, theta)+            Nothing -> Nothing+      p _ = Nothing+      lhs2 = neg inf2+      rhs2 = pos inf2++-- |Unification: unifies two sentences.+unify :: Literal formula term v p f => formula -> formula -> Maybe (Subst v term, Subst v term)+unify s1 s2 = unify' s1 s2 empty empty++unify' :: Literal formula term v p f =>+          formula -> formula -> Subst v term -> Subst v term -> Maybe (Subst v term, Subst v term)+unify' f1 f2 theta1 theta2 =+    zipLiterals+         (\ _ _ -> error "unify'")+         (\ pa1 pa2 ->+              case (pa1, pa2) of+                (EqualLit l1 r1, EqualLit l2 r2) -> unifyTerms [l1, r1] [l2, r2] theta1 theta2+                (ApplyLit p1 ts1, ApplyLit p2 ts2) -> if p1 == p2 then unifyTerms ts1 ts2 theta1 theta2 else Nothing+                _ -> Nothing)+         f1 f2++unifyTerm :: Term term v f => term -> term -> Subst v term -> Subst v term -> Maybe (Subst v term, Subst v term)+unifyTerm t1 t2 theta1 theta2 =+    foldTerm+          (\ v1 ->+               maybe (Just (M.insert v1 t2 theta1, theta2))+                     (\ t1' -> unifyTerm t1' t2 theta1 theta2)+                     (M.lookup v1 theta1))+          (\ f1 ts1 ->+               foldTerm (\ v2 -> maybe (Just (theta1, M.insert v2 t1 theta2))+                                 (\ t2' -> unifyTerm t1 t2' theta1 theta2)+                                 (M.lookup v2 theta2))+                        (\ f2 ts2 -> if f1 == f2+                                     then unifyTerms ts1 ts2 theta1 theta2+                                     else Nothing)+                        t2)+          t1++unifyTerms :: Term term v f =>+              [term] -> [term] -> Subst v term -> Subst v term -> Maybe (Subst v term, Subst v term)+unifyTerms [] [] theta1 theta2 = Just (theta1, theta2)+unifyTerms (t1:ts1) (t2:ts2) theta1 theta2 =+    case (unifyTerm t1 t2 theta1 theta2) of+      Nothing                -> Nothing+      Just (theta1',theta2') -> unifyTerms ts1 ts2 theta1' theta2'+unifyTerms _ _ _ _ = Nothing++findUnify :: forall formula term v p f. (Literal formula term v p f, Term term v f) =>+             term -> term -> S.Set formula -> Maybe ((term, term), Subst v term, Subst v term)+findUnify tl tr s =+    let+      terms = concatMap (foldLiteral (\ (_ :: formula) -> error "getTerms") p) (S.toList s)+      unifiedTerms' = map (\t -> unifyTerm tl t empty empty) terms+      unifiedTerms = filter isJust unifiedTerms'+    in+     case unifiedTerms of+       [] -> Nothing+       (Just (theta1, theta2)):_ ->+         Just ((substTerm tl theta1, substTerm tr theta1), theta1, theta2)+       (Nothing:_) -> error "findUnify"+    where+      -- getTerms formula = foldLiteral (\ _ -> error "getTerms") p formula+      p :: PredicateLit p term -> [term]+      p (EqualLit t1 t2) = getTerms' t1 ++ getTerms' t2+      p (ApplyLit _ ts) = concatMap getTerms' ts+      getTerms' :: term -> [term]+      getTerms' t = foldTerm (\ v -> [var v]) (\ f ts -> fApp f ts : concatMap getTerms' ts) t++{-+getTerms :: Literal formula term v p f => formula -> [term]+getTerms formula =+    foldLiteral (\ _ -> error "getTerms") p formula+    where+      getTerms' t = foldT (\ v -> [var v]) (\ f ts -> fApp f ts : concatMap getTerms' ts) t+      p (Equal t1 t2) = getTerms' t1 ++ getTerms' t2+      p (Apply _ ts) = concatMap getTerms' ts+-}++replaceTerm :: (Literal lit term v p f) => lit -> (term, term) -> Maybe lit+replaceTerm formula (tl', tr') =+    foldLiteral+          (\ _ -> error "error in replaceTerm")+          (\ pa -> case pa of+                     EqualLit t1 t2 ->+                         let t1' = replaceTerm' t1+                             t2' = replaceTerm' t2 in+                         if t1' == t2' then Nothing else Just (t1' `equals` t2')+                     ApplyLit p ts -> Just (pAppLiteral p (map (\ t -> replaceTerm' t) ts)))+          formula+    where+      replaceTerm' t =+          if termEq t tl'+          then tr'+          else foldTerm var (\ f ts -> fApp f (map replaceTerm' ts)) t+      termEq t1 t2 =+          maybe False id (zipT (\ v1 v2 -> Just (v1 == v2)) (\ f1 ts1 f2 ts2 -> Just (f1 == f2 && length ts1 == length ts2 && all (uncurry termEq) (zip ts1 ts2))) t1 t2)++subst :: Literal formula term v p f => formula -> Subst v term -> Maybe formula+subst formula theta =+    foldLiteral+          (\ _ -> Just formula)+          (\ pa -> case pa of+                     EqualLit t1 t2 ->+                         let t1' = substTerm t1 theta+                             t2' = substTerm t2 theta in+                         if t1' == t2' then Nothing else Just (t1' `equals` t2')+                     ApplyLit p ts -> Just (pAppLiteral p (substTerms ts theta)))+          formula++substTerm :: Term term v f => term -> Subst v term -> term+substTerm term theta =+    foldTerm (\ v -> maybe term id (M.lookup v theta))+             (\ f ts -> fApp f (substTerms ts theta))+             term++substTerms :: Term term v f => [term] -> Subst v term -> [term]+substTerms ts theta = map (\t -> substTerm t theta) ts++updateSubst :: Term term v f => Subst v term -> Subst v term -> Subst v term+updateSubst theta1 theta2 = M.union theta1 (M.intersection theta1 theta2)+-- This is what was in the original code, which behaves slightly differently+--updateSubst theta1 _ | M.null theta1 = M.empty+--updateSubst theta1 theta2 = M.unionWith (\ _ term2 -> term2) theta1 theta2
+ Data/Logic/Satisfiable.hs view
@@ -0,0 +1,44 @@+-- |Do satisfiability computations on any FirstOrderFormula formula by+-- converting it to a convenient instance of PropositionalFormula and+-- using the satisfiable function from that instance.  Currently we+-- use the satisfiable function from the PropLogic package, by the+-- Bucephalus project.+{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, ScopedTypeVariables #-}+module Data.Logic.Satisfiable+    ( satisfiable+    , theorem+    , inconsistant+    , invalid+    ) where++import qualified Data.Set as Set+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), toPropositional)+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Classes.Negatable ((.~.))+import Data.Logic.Instances.PropLogic ()+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (NormalT)+import qualified PropLogic as PL++-- |Is there any variable assignment that makes the formula true?+satisfiable :: forall formula term v p f m. (Monad m, FirstOrderFormula formula term v p f, Ord formula, Literal formula term v p f) =>+                formula -> NormalT v term m Bool+satisfiable f =+    do (clauses :: Set.Set (Set.Set formula)) <- clauseNormalForm f+       let f' = PL.CJ . map (PL.DJ . map (toPropositional PL.A)) . map Set.toList . Set.toList $ clauses+       return . PL.satisfiable $ f'++-- |Is the formula always false?  (Not satisfiable.)+inconsistant :: (Monad m, FirstOrderFormula formula term v p f, Ord formula, Literal formula term v p f) =>+                formula -> NormalT v term m Bool+inconsistant f =  satisfiable f >>= return . not++-- |Is the negation of the formula inconsistant?+theorem :: (Monad m, FirstOrderFormula formula term v p f, Ord formula, Literal formula term v p f) =>+           formula -> NormalT v term m Bool+theorem f = inconsistant ((.~.) f)++-- |A formula is invalid if it is neither a theorem nor inconsistent.+invalid :: (Monad m, FirstOrderFormula formula term v p f, Ord formula, Literal formula term v p f) =>+           formula -> NormalT v term m Bool+invalid f = inconsistant f >>= \ fi -> theorem f >>= \ ft -> return (not (fi || ft))
+ Data/Logic/Test.hs view
@@ -0,0 +1,243 @@+-- |Types to use for creating test cases.  These are used in the Logic+-- package test cases, and are exported for use in its clients.+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, RankNTypes, ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wwarn #-}+module Data.Logic.Test+    ( -- * Formula parameter types+      V(..)+    , Pr(..)+    , AtomicFunction(..)+    , TFormula+    , TTerm+    , prettyV+    , prettyP+    , prettyF+      -- * Test case types+    , TestFormula(..)+    , Expected(..)+    , doTest+    , TestProof(..)+    , ProofExpected(..)+    , doProof+    ) where++import Control.Monad.Reader (MonadPlus(..), msum)+import Data.Boolean.SatSolver (CNF)+import Data.Char (isDigit)+import Data.Generics (Data, Typeable, listify)+--import Data.Logic.Clause (ClauseNormalFormula(satisfiable))+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.ClauseNormalForm (ClauseNormalFormula(satisfiable))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula, convertFOF)+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Variable (Variable(one, next))+--import qualified Data.Logic.Instances.Chiou as C+import qualified Data.Logic.Types.FirstOrder as P+import Data.Logic.Instances.PropLogic (plSat)+import qualified Data.Logic.Instances.SatSolver as SS+import Data.Logic.KnowledgeBase (WithId, runProver', Proof, loadKB, theoremKB, getKB)+import Data.Logic.Normal.Clause (clauseNormalForm, trivial)+import Data.Logic.Normal.Negation (negationNormalForm, simplify)+import Data.Logic.Normal.Prenex (prenexNormalForm)+import Data.Logic.Normal.Implicative (ImplicativeForm)+import Data.Logic.Normal.Skolem (skolemNormalForm, runNormal, runNormal', runNormalT')+import Data.Logic.Classes.Arity (Arity(arity))+import Data.Logic.Resolution (SetOfSupport)+import qualified Data.Set as S+import Data.String (IsString(fromString))++--import PropLogic (PropForm)++import Test.HUnit+import Text.PrettyPrint (Doc, text)++newtype V = V String deriving (Eq, Ord, Data, Typeable)++instance IsString V where+    fromString = V++instance Show V where+    show (V s) = show s++prettyV :: V -> Doc+prettyV (V s) = text s++instance Variable V where+    one = V "x"+    next (V s) =+        V (case break (not . isDigit) (reverse s) of+             (_, "") -> "x"+             ("", nondigits) -> nondigits ++ "2"+             (digits, nondigits) -> nondigits ++ show (1 + read (reverse digits) :: Int))+        +-- |A newtype for the Primitive Predicate parameter.+data Pr+    = Pr String+    | T+    | F+    | Equals+    deriving (Eq, Ord, Data, Typeable)++instance IsString Pr where+    fromString = Pr++instance Boolean Pr where+    fromBool True = T+    fromBool False = F++instance Arity Pr where+    arity (Pr _) = Nothing+    arity T = Just 0+    arity F = Just 0+    arity Equals = Just 2++instance Show Pr where+    show T = "fromBool True"+    show F = "fromBool False"+    show Equals = ".=."+    show (Pr s) = show s            -- Because Pr is an instance of IsString++prettyP :: Pr -> Doc+prettyP T = text "True"+prettyP F = text "False"+prettyP Equals = text ".=."+prettyP (Pr s) = text s++data AtomicFunction+    = Fn String+    | Skolem Int+    deriving (Eq, Ord, Data, Typeable)++instance Skolem AtomicFunction where+    toSkolem = Skolem+    fromSkolem (Skolem n) = Just n+    fromSkolem _ = Nothing++instance IsString AtomicFunction where+    fromString = Fn++instance Show AtomicFunction where+    show (Fn s) = show s+    show (Skolem n) = "toSkolem " ++ show n++prettyF :: AtomicFunction -> Doc+prettyF (Fn s) = text s+prettyF (Skolem n) = text ("sK" ++ show n)++type TFormula = P.Formula V Pr AtomicFunction+type TTerm = P.PTerm V AtomicFunction++-- |This allows you to use an expression that returns the Doc type in a+-- unit test, such as prettyFirstOrder.+instance Eq Doc where+    a == b = show a == show b++data TestFormula formula term v p f+    = TestFormula+      { formula :: formula+      , name :: String+      , expected :: [Expected formula term v p f]+      } deriving (Data, Typeable)++-- |Some values that we might expect after transforming the formula.+data (FirstOrderFormula formula term v p f) => Expected formula term v p f+    = FirstOrderFormula formula+    | SimplifiedForm formula+    | NegationNormalForm formula+    | PrenexNormalForm formula+    | SkolemNormalForm formula+    | SkolemNumbers (S.Set Int)+    | ClauseNormalForm (S.Set (S.Set formula))+    | TrivialClauses [(Bool, (S.Set formula))]+    | ConvertToChiou formula+    | ChiouKB1 (Proof formula)+    | PropLogicSat Bool+    | SatSolverCNF CNF+    | SatSolverSat Bool+    deriving (Data, Typeable)++doTest :: (FirstOrderFormula formula term v p f, Literal formula term v p f, Data formula, Show term, Show formula) =>+          TestFormula formula term v p f -> Test+doTest f =+    TestLabel (name f) $ TestList $ +    map doExpected (expected f)+    where+      doExpected (FirstOrderFormula f') =+          TestCase (assertEqual (name f ++ " original formula") (p f') (p (formula f)))+      doExpected (SimplifiedForm f') =+          TestCase (assertEqual (name f ++ " simplified") (p f') (p (simplify (formula f))))+      doExpected (PrenexNormalForm f') =+          TestCase (assertEqual (name f ++ " prenex normal form") (p f') (p (prenexNormalForm (formula f))))+      doExpected (NegationNormalForm f') =+          TestCase (assertEqual (name f ++ " negation normal form") (p f') (p (negationNormalForm (formula f))))+      doExpected (SkolemNormalForm f') =+          TestCase (assertEqual (name f ++ " skolem normal form") (p f') (p (runNormal (skolemNormalForm (formula f)))))+      doExpected (SkolemNumbers f') =+          TestCase (assertEqual (name f ++ " skolem numbers") f' (skolemSet (runNormal (skolemNormalForm (formula f)))))+      doExpected (ClauseNormalForm fss) =+          TestCase (assertEqual (name f ++ " clause normal form") fss (S.map (S.map p) (runNormal (clauseNormalForm (formula f)))))+      doExpected (TrivialClauses flags) =+          TestCase (assertEqual (name f ++ " trivial clauses") flags (map (\ x -> (trivial x, x)) (S.toList (runNormal (clauseNormalForm (formula f))))))+      doExpected (ConvertToChiou result) =+          TestCase (assertEqual (name f ++ " converted to Chiou") result (convertFOF id id id (formula f)))+      doExpected (ChiouKB1 result) =+          TestCase (assertEqual (name f ++ " Chiou KB") result (runProver' (loadKB [formula f] >>= return . head)))+      doExpected (PropLogicSat result) =+          TestCase (assertEqual (name f ++ " PropLogic.satisfiable") result (runNormal (plSat (formula f))))+      doExpected (SatSolverCNF result) =+          TestCase (assertEqual (name f ++ " SatSolver CNF") (norm result) (runNormal' (SS.toCNF (formula f))))+      doExpected (SatSolverSat result) =+          TestCase (assertEqual (name f ++ " SatSolver CNF") result (null (runNormalT' (SS.toCNF (formula f) >>= satisfiable))))+      p = id++      norm = map S.toList . S.toList . S.fromList . map S.fromList++skolemSet :: (FirstOrderFormula formula term v p f, Data f, Typeable f, Data formula) => formula -> S.Set Int+skolemSet =+    foldr ins S.empty . skolemList+    where+      ins f s = case fromSkolem f of+                  Just n -> S.insert n s+                  Nothing -> s+      skolemList :: (FirstOrderFormula formula term v p f, Data f, Typeable f, Data formula) => formula -> [f]+      skolemList inf = gFind inf :: (Typeable f => [f])++-- | @gFind a@ will extract any elements of type @b@ from+-- @a@'s structure in accordance with the MonadPlus+-- instance, e.g. Maybe Foo will return the first Foo+-- found while [Foo] will return the list of Foos found.+gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b+gFind = msum . map return . listify (const True)++data TestProof formula term v+    = TestProof+      { proofName :: String+      , proofKnowledge :: (String, [formula])+      , conjecture :: formula+      , proofExpected :: [ProofExpected formula v term]+      } deriving (Data, Typeable)++data ProofExpected formula v term+    = ChiouResult (Bool, SetOfSupport formula v term)+    | ChiouKB (S.Set (WithId (ImplicativeForm formula)))+    deriving (Data, Typeable)++doProof :: forall formula term v p f. (FirstOrderFormula formula term v p f, Literal formula term v p f, Eq term, Show term, Show v, Show formula) =>+           TestProof formula term v -> Test+doProof p =+    TestLabel (proofName p) $ TestList $+    concatMap doExpected (proofExpected p)+    where+      doExpected (ChiouResult result) =+          [TestLabel (proofName p ++ " with " ++ fst (proofKnowledge p)) . TestList $+           [TestCase (assertEqual (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " using Chiou prover")+                      result+                      (runProver' (loadKB kb >> theoremKB c)))]]+      doExpected (ChiouKB result) =+          [TestLabel (proofName p ++ " with " ++ fst (proofKnowledge p)) . TestList $+           [TestCase (assertEqual (proofName p ++ " with " ++ fst (proofKnowledge p) ++ " Chiou knowledge base")+                      result+                      (runProver' (loadKB kb >> getKB)))]]+      kb = snd (proofKnowledge p) :: [formula]+      c = conjecture p :: formula
+ Data/Logic/Types/FirstOrder.hs view
@@ -0,0 +1,160 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, FunctionalDependencies,+             GeneralizedNewtypeDeriving, MultiParamTypeClasses, TemplateHaskell, UndecidableInstances #-}+{-# OPTIONS -fno-warn-missing-signatures -fno-warn-orphans #-}+-- |Data types which are instances of the Logic type class for use+-- when you just want to use the classes and you don't have a+-- particular representation you need to use.+module Data.Logic.Types.FirstOrder+    ( Formula(..)+    , PTerm(..)+    ) where++import Data.Data (Data)+import Data.Logic.Classes.Arity (Arity)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), showFirstOrder, Quant(..), Predicate(..))+import Data.Logic.Classes.Literal (Literal(..), PredicateLit(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable(Negatable(..))+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Classes.Propositional (Combine(..), BinOp(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..), showTerm)+import Data.Logic.Classes.Variable (Variable)+import Data.Logic.Classes.Propositional (PropositionalFormula(..))+import Data.SafeCopy (base, deriveSafeCopy)+import Data.Typeable (Typeable)+import Happstack.Data (deriveNewData)++-- | The range of a formula is {True, False} when it has no free variables.+data Formula v p f+    = Predicate (Predicate p (PTerm v f))+    | Combine (Combine (Formula v p f))+    | Quant Quant v (Formula v p f)+    -- Note that a derived Eq instance is not going to tell us that+    -- a&b is equal to b&a, let alone that ~(a&b) equals (~a)|(~b).+    deriving (Eq,Ord,Read,Data,Typeable)++-- | The range of a term is an element of a set.+data PTerm v f+    = Var v                         -- ^ A variable, either free or+                                    -- bound by an enclosing quantifier.+    | FunApp f [PTerm v f]           -- ^ Function application.+                                    -- Constants are encoded as+                                    -- nullary functions.  The result+                                    -- is another term.+    deriving (Eq,Ord,Read,Data,Typeable)++-- data InfixPred = (:=:) | (:!=:) deriving (Eq,Ord,Show,Data,Typeable,Enum,Bounded)++-- |We need to implement read manually here due to+-- <http://hackage.haskell.org/trac/ghc/ticket/4136>+{-+instance Read InfixPred where+    readsPrec _ s =+        map (\ (x, t) -> (x, drop (length t) s))+            (take 1 (dropWhile (\ (_, t) -> not (isPrefixOf t s)) prs))+        where+          prs = [((:=:), ":=:"),+                 ((:!=:), ":!=:")]+-}++instance (FirstOrderFormula (Formula v p f) (PTerm v f) v p f, Show v, Show p, Show f) => Show (Formula v p f) where+    show = showFirstOrder++instance (FirstOrderFormula (Formula v p f) (PTerm v f) v p f, Show v, Show p, Show f) => Show (PTerm v f) where+    show = showTerm++instance Negatable (Formula v p f) where+    (.~.) (Combine ((:~:) (Combine ((:~:) x)))) = (.~.) x+    (.~.) (Combine ((:~:) x)) = x+    (.~.) x = Combine ((:~:) x)+    negated (Combine ((:~:) x)) = not (negated x)+    negated _ = False++instance (Ord v, Ord p, Ord f) => Logic (Formula v p f) where+    x .<=>. y = Combine (BinOp  x (:<=>:) y)+    x .=>.  y = Combine (BinOp  x (:=>:)  y)+    x .|.   y = Combine (BinOp  x (:|:)   y)+    x .&.   y = Combine (BinOp  x (:&:)   y)++instance (Ord v, Variable v, Data v,+          Ord p, Boolean p, Arity p, Data p,+          Ord f, Skolem f, Data f,+          Boolean (Formula v p f), Logic (Formula v p f)) =>+         PropositionalFormula (Formula v p f) (Formula v p f) where+    atomic (Predicate (Equal t1 t2)) = t1 .=. t2+    atomic (Predicate (NotEqual t1 t2)) = t1 .!=. t2+    atomic (Predicate (Apply p ts)) = pApp p ts+    atomic _ = error "atomic method of PropositionalFormula for Parameterized: invalid argument"+    foldPropositional c a formula =+        case formula of+          Quant _ _ _ -> error "foldF0: quantifiers should not be present"+          Combine x -> c x+          Predicate x -> a (Predicate x)++instance (Ord v, Variable v, Data v, Eq f, Ord f, Skolem f, Data f) => Term (PTerm v f) v f where+    foldTerm vf fn t =+        case t of+          Var v -> vf v+          FunApp f ts -> fn f ts+    zipT v f t1 t2 =+        case (t1, t2) of+          (Var v1, Var v2) -> v v1 v2+          (FunApp f1 ts1, FunApp f2 ts2) -> f f1 ts1 f2 ts2+          _ -> Nothing+    var = Var+    fApp x args = FunApp x args++instance (Ord v, Ord p, Boolean p, Arity p, Ord f) => Pred p (PTerm v f) (Formula v p f) where+    pApp0 x = Predicate (Apply x [])+    pApp1 x a = Predicate (Apply x [a])+    pApp2 x a b = Predicate (Apply x [a,b])+    pApp3 x a b c = Predicate (Apply x [a,b,c])+    pApp4 x a b c d = Predicate (Apply x [a,b,c,d])+    pApp5 x a b c d e = Predicate (Apply x [a,b,c,d,e])+    pApp6 x a b c d e f = Predicate (Apply x [a,b,c,d,e,f])+    pApp7 x a b c d e f g = Predicate (Apply x [a,b,c,d,e,f,g])+    x .=. y = Predicate (Equal x y)+    x .!=. y = Predicate (NotEqual x y)++instance (Pred p (PTerm v f) (Formula v p f),+          Variable v, Ord v, Data v, Show v,+          Ord p, Data p, Show p,+          Skolem f, Ord f, Data f, Show f) =>+         FirstOrderFormula (Formula v p f) (PTerm v f) v p f where+    for_all v x = Quant All v x+    exists v x = Quant Exists v x+    foldFirstOrder q c p f =+        case f of+          Quant op v f' -> q op v f'+          Combine x -> c x+          Predicate x -> p x+    zipFirstOrder q c p f1 f2 =+        case (f1, f2) of+          (Quant q1 v1 f1', Quant q2 v2 f2') -> q q1 v1 (Quant q1 v1 f1') q2 v2 (Quant q2 v2 f2')+          (Combine x, Combine y) -> c x y+          (Predicate x, Predicate y) -> p x y+          _ -> Nothing++instance (Variable v, Ord v, Data v, Show v,+          Arity p, Boolean p, Ord p, Data p, Show p,+          Skolem f, Ord f, Data f, Show f) => Literal (Formula v p f) (PTerm v f) v p f where+    equals x y = Predicate (Equal x y)+    pAppLiteral p ts = Predicate (Apply p ts)+    foldLiteral c pr l =+        case l of+          (Combine ((:~:) x)) -> c x+          (Predicate (Apply p ts)) -> pr (ApplyLit p ts)+          (Predicate (Equal x y)) -> pr (EqualLit x y)+          _ -> error "Invalid formula used as Literal instance"+    zipLiterals c pr l1 l2 =+        case (l1, l2) of+          (Combine ((:~:) x), Combine ((:~:) y)) -> c x y+          (Predicate (Apply p1 ts1), Predicate (Apply p2 ts2)) -> pr (ApplyLit p1 ts1) (ApplyLit p2 ts2)+          _ -> Nothing++$(deriveSafeCopy 1 'base ''PTerm)+$(deriveSafeCopy 1 'base ''Formula)++$(deriveNewData [''PTerm, ''Formula])
+ Data/Logic/Types/FirstOrderPublic.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GeneralizedNewtypeDeriving,+             MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, UndecidableInstances #-}+{-# OPTIONS -Wwarn -fno-warn-orphans #-}+-- |An instance of FirstOrderFormula which implements Eq and Ord by comparing+-- after conversion to normal form.  This helps us notice that formula which+-- only differ in ways that preserve identity, e.g. swapped arguments to a+-- commutative operator.++module Data.Logic.Types.FirstOrderPublic+    ( Formula(..)+    , N.PTerm(..)+    , Bijection(..)+    ) where++import Data.Data (Data)+import Data.Logic.Classes.Arity (Arity)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))+import qualified Data.Logic.Types.FirstOrder as N+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Pred (Pred(..))+import Data.Logic.Classes.Propositional (Combine(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..), )+import Data.Logic.Classes.Variable (Variable)+import Data.Logic.Normal.Implicative (implicativeNormalForm, ImplicativeForm)+import Data.Logic.Normal.Skolem (runNormal)+import Data.SafeCopy (base, deriveSafeCopy)+import Data.Set (Set)+import Data.Typeable (Typeable)+import Happstack.Data (deriveNewData)++class Bijection p i where+    public :: i -> p+    intern :: p -> i++-- |The new Formula type is just a wrapper around the Native instance+-- (which eventually should be renamed the Internal instance.)  No+-- derived Eq or Ord instances.+data Formula v p f = Formula {unFormula :: N.Formula v p f} deriving (Read, Data, Typeable)++instance Bijection (Formula v p f) (N.Formula v p f) where+    public = Formula+    intern = unFormula++instance Bijection (Combine (Formula v p f)) (Combine (N.Formula v p f)) where+    public (BinOp x op y) = BinOp (public x) op (public y)+    public ((:~:) x) = (:~:) (public x)+    intern (BinOp x op y) = BinOp (intern x) op (intern y)+    intern ((:~:) x) = (:~:) (intern x)++instance Negatable (Formula v p f) where+    negated = negated . unFormula+    (.~.) = Formula . (.~.) . unFormula++instance (Variable v, Show v, Ord v, Data v,+          Arity p, Boolean p, Show p, Ord p, Data p,+          Skolem f, Show f, Ord f, Data f) => Logic (Formula v p f) where+    x .<=>. y = Formula $ (unFormula x) .<=>. (unFormula y)+    x .=>.  y = Formula $ (unFormula x) .=>. (unFormula y)+    x .|.   y = Formula $ (unFormula x) .|. (unFormula y)+    x .&.   y = Formula $ (unFormula x) .&. (unFormula y)++instance (Arity p, Variable v, Skolem f, Boolean p,+          Show p, Show v, Show f,+          Ord f, Ord v, Ord p,+          Data p, Data v, Data f) => Show (Formula v p f) where+    showsPrec n x = showsPrec n (unFormula x)++instance (Variable v, Show v, Ord v, Data v,+          Show p, Ord p, Data p, Boolean p, Arity p,+          Skolem f, Show f, Ord f, Data f) => Pred p (N.PTerm v f) (Formula v p f) where+    pApp0 p = (public :: N.Formula v p f -> Formula v p f) $ pApp0 p+    pApp1 p t1 = (public :: N.Formula v p f -> Formula v p f) $ pApp1 p (t1)+    pApp2 p t1 t2 = (public :: N.Formula v p f -> Formula v p f) $ pApp2 p (t1) (t2)+    pApp3 p t1 t2 t3 = (public :: N.Formula v p f -> Formula v p f) $ pApp3 (p) (t1) (t2) (t3)+    pApp4 p t1 t2 t3 t4 = (public :: N.Formula v p f -> Formula v p f) $ pApp4 (p) (t1) (t2) (t3) (t4)+    pApp5 p t1 t2 t3 t4 t5 = (public :: N.Formula v p f -> Formula v p f) $ pApp5 (p) (t1) (t2) (t3) (t4) (t5)+    pApp6 p t1 t2 t3 t4 t5 t6 = (public :: N.Formula v p f -> Formula v p f) $ pApp6 (p) (t1) (t2) (t3) (t4) (t5) (t6)+    pApp7 p t1 t2 t3 t4 t5 t6 t7 = (public :: N.Formula v p f -> Formula v p f) $ pApp7 (p) (t1) (t2) (t3) (t4) (t5) (t6) (t7)+    t1 .=. t2 = (public :: N.Formula v p f -> Formula v p f) $ (t1) .=. (t2)++instance (Logic (Formula v p f), Term (N.PTerm v f) v f,+          Show v,+          Arity p, Boolean p, Ord p, Data p, Show p,+          Ord f, Show f) => FirstOrderFormula (Formula v p f) (N.PTerm v f) v p f where+    for_all v x = public $ for_all v (intern x :: N.Formula v p f)+    exists v x = public $ exists v (intern x :: N.Formula v p f)+    foldFirstOrder q c p f = foldFirstOrder q' c' p (intern f :: N.Formula v p f)+        where q' quant v form = q quant v (public form)+              c' x = c (public x)+    zipFirstOrder q c p f1 f2 = zipFirstOrder q' c' p (intern f1 :: N.Formula v p f) (intern f2 :: N.Formula v p f)+        where q' q1 v1 f1' q2 v2 f2' = q q1 v1 (public f1') q2 v2 (public f2')+              c' combine1 combine2 = c (public combine1) (public combine2)++-- |Here are the magic Ord and Eq instances+instance (FirstOrderFormula (Formula v p f) (N.PTerm v f) v p f,+          Literal (N.Formula v p f) (N.PTerm v f) v p f,+          FirstOrderFormula (N.Formula v p f) (N.PTerm v f) v p f,+          Ord (N.Formula v p f)) => Ord (Formula v p f) where+    compare a b =+        let (a' :: Set (ImplicativeForm (N.Formula v p f))) = runNormal (implicativeNormalForm (intern a :: N.Formula v p f))+            (b' :: Set (ImplicativeForm (N.Formula v p f))) = runNormal (implicativeNormalForm (intern b :: N.Formula v p f)) in+        case compare a' b' of+          EQ -> EQ+          x -> {- if isRenameOf a' b' then EQ else -} x++instance (FirstOrderFormula (Formula v p f) (N.PTerm v f) v p f) => Eq (Formula v p f) where+    a == b = compare a b == EQ++$(deriveSafeCopy 1 'base ''Formula)++$(deriveNewData [''Formula])
+ Data/Logic/Types/Propositional.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses #-}+module Data.Logic.Types.Propositional where++import Data.Generics (Data, Typeable)+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Propositional (PropositionalFormula(..), Combine(..), BinOp(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Boolean (Boolean(..))++-- | The range of a formula is {True, False} when it has no free variables.+data Formula atom+    = Combine (Combine (Formula atom))+    | Atom atom+    -- Note that a derived Eq instance is not going to tell us that+    -- a&b is equal to b&a, let alone that ~(a&b) equals (~a)|(~b).+    deriving (Eq,Ord,Read,Data,Typeable)++instance Negatable (Formula atom) where+    (.~.) (Combine ((:~:) (Combine ((:~:) x)))) = (.~.) x+    (.~.) (Combine ((:~:) x)) = x+    (.~.) x = Combine ((:~:) x)+    negated (Combine ((:~:) x)) = not (negated x)+    negated _ = False++instance Ord atom => Logic (Formula atom) where+    x .<=>. y = Combine (BinOp  x (:<=>:) y)+    x .=>.  y = Combine (BinOp  x (:=>:)  y)+    x .|.   y = Combine (BinOp  x (:|:)   y)+    x .&.   y = Combine (BinOp  x (:&:)   y)++instance Boolean atom => Boolean (Formula atom) where+    fromBool = Atom . fromBool++instance (Boolean atom, Ord atom) => PropositionalFormula (Formula atom) atom where+    atomic a = Atom a+    foldPropositional c a formula =+        case formula of+          Combine x -> c x+          Atom x -> a x+{-+    asBool (Atom x) =+        if x == fromBool True+        then Just True+        else if x == fromBool False+             then Just False+             else Nothing+    asBool (Combine _) = Nothing+-}
+ Setup.hs view
@@ -0,0 +1,20 @@+#!/usr/bin/env runghc++module Main where++import Distribution.Simple+import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(buildDir))+import Distribution.Simple.Program+import System.Cmd+import System.Exit+import System.Posix.Files (fileExist)++main :: IO ()+main = defaultMainWithHooks simpleUserHooks {+         postBuild = \ _ _ _ lbi -> runTestScript lbi+       , runTests = \ _ _ _ lbi -> runTestScript lbi+       }++runTestScript lbi =+    system (buildDir lbi ++ "/tests/tests") >>= \ code ->+    if code == ExitSuccess then return () else error "Test Failure"
+ Test/Chiou0.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE OverloadedStrings, StandaloneDeriving #-}+{-# OPTIONS -fno-warn-orphans #-}++module Test.Chiou0 where++import Control.Monad.Identity (runIdentity)+import Control.Monad.Trans (MonadIO, liftIO)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Pred (pApp)+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.KnowledgeBase (ProverT, runProver', Proof(..), ProofResult(..), loadKB, theoremKB {-, askKB, showKB-})+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')+import Data.Logic.Normal.Skolem (NormalT, runNormal)+import Data.Logic.Resolution (SetOfSupport)+import Data.Logic.Test (V(..), Pr(..), AtomicFunction(..), TFormula, TTerm)+import Data.Logic.Types.FirstOrder (Formula, PTerm)+import Data.Map (fromList)+import qualified Data.Set as S+import Data.String (IsString(..))+import Test.HUnit++tests :: Test+tests = TestLabel "Chiou0" $ TestList [loadTest, proofTest1, proofTest2]++loadTest :: Test+loadTest =+    TestCase (assertEqual "Chiuo0 - loadKB test" expected (runProver' (loadKB sentences)))+    where+      expected :: [Proof TFormula]+      expected = [Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem 1) []])]),+                                             makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])])]),+                  Proof Invalid (S.fromList [makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [var ("x"),var ("y")])]) ([(pApp ("AnimalLover") [var ("x")])])]),+                  Proof Invalid (S.fromList [makeINF' ([(pApp ("Animal") [var ("y")]),(pApp ("AnimalLover") [var ("x")]),(pApp ("Kills") [var ("x"),var ("y")])]) ([])]),+                  Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])])]),+                  Proof Invalid (S.fromList [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])])]),+                  Proof Invalid (S.fromList [makeINF' ([(pApp ("Cat") [var ("x")])]) ([(pApp ("Animal") [var ("x")])])])]++proofTest1 :: Test+proofTest1 = TestCase (assertEqual "Chiuo0 - proof test 1" proof1 (runProver' (loadKB sentences >> theoremKB (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []] :: TFormula))))++inf' l1 l2 = INF (S.fromList l1) (S.fromList l2)++proof1 :: (Bool, SetOfSupport TFormula V TTerm)+proof1 = (False,+          (S.fromList+           [(makeINF' ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]) ([]),fromList []),+            (makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]),fromList []),+            (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Curiosity") []])]) ([]),fromList []),+            (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+            (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+            (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+            (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+            (makeINF' ([(pApp ("AnimalLover") [fApp ("Curiosity") []])]) ([]),fromList []),+            (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+            (makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList []),+            (makeINF' ([(pApp ("Owns") [fApp ("Curiosity") [],var ("y")])]) ([]),fromList [])]))++proofTest2 :: Test+proofTest2 = TestCase (assertEqual "Chiuo0 - proof test 2" proof2 (runProver' (loadKB sentences >> theoremKB conjecture)))+    where+      conjecture :: TFormula+      conjecture = (pApp "Kills" [fApp "Curiosity" [], fApp (Fn "Tuna") []])++proof2 :: (Bool, SetOfSupport TFormula V TTerm)+proof2 = (True,+          S.fromList+          [(makeINF' ([]) ([]),fromList []),+           (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),+           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),+           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+           (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+           (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Dog") [var ("y2")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+           (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])++testProof :: MonadIO m => String -> (TFormula, Bool, (S.Set (ImplicativeForm TFormula))) -> ProverT (ImplicativeForm TFormula) (NormalT V TTerm m) ()+testProof label (question, expectedAnswer, expectedProof) =+    theoremKB question >>= \ (actualFlag, actualProof) ->+    let actual' = (actualFlag, S.map fst actualProof) in+    if actual' /= (expectedAnswer, expectedProof)+    then error ("\n Expected:\n  " ++ show (expectedAnswer, expectedProof) +++                "\n Actual:\n  " ++ show actual')+    else liftIO (putStrLn (label ++ " ok"))++loadCmd :: Monad m => ProverT (ImplicativeForm TFormula) (NormalT V TTerm m) [Proof TFormula]+loadCmd = loadKB sentences++sentences :: [TFormula]+sentences = [exists "x" ((pApp "Dog" [var "x"]) .&. (pApp "Owns" [fApp "Jack" [], var "x"])),+             for_all "x" (((exists "y" (pApp "Dog" [var "y"])) .&. (pApp "Owns" [var "x", var "y"])) .=>. (pApp "AnimalLover" [var "x"])),+             for_all "x" ((pApp "AnimalLover" [var "x"]) .=>. (for_all "y" ((pApp "Animal" [var "y"]) .=>. ((.~.) (pApp "Kills" [var "x", var "y"]))))),+             (pApp "Kills" [fApp "Jack" [], fApp "Tuna" []]) .|. (pApp "Kills" [fApp "Curiosity" [], fApp "Tuna" []]),+             pApp "Cat" [fApp "Tuna" []],+             for_all "x" ((pApp "Cat" [var "x"]) .=>. (pApp "Animal" [var "x"]))]
+ Test/Data.hs view
@@ -0,0 +1,1077 @@+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, MonoLocalBinds, NoMonomorphismRestriction, OverloadedStrings, RankNTypes, ScopedTypeVariables  #-}+{-# OPTIONS -fno-warn-name-shadowing -fno-warn-missing-signatures #-}+module Test.Data+    ( tests+    , allFormulas+    , proofs+{-+    , formulas+    , animalKB+    , animalConjectures+    , chang43KB+    , chang43Conjecture+    , chang43ConjectureRenamed+-}+    ) where++import Data.Boolean.SatSolver (Literal(..))+import Data.Generics (Typeable)+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), for_all', exists', convertFOF)+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.Classes.Skolem (Skolem(toSkolem))+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Classes.Negatable (Negatable(..))+import qualified Data.Logic.Classes.Literal as N+import qualified Data.Logic.Instances.Chiou as C+import Data.Logic.KnowledgeBase (WithId(WithId, wiItem, wiIdent), Proof(..), ProofResult(..))+import Data.Logic.Normal.Implicative (ImplicativeForm(INF), makeINF')+import Data.Logic.Test (TestFormula(..), TestProof(..), Expected(..), ProofExpected(..), doTest, doProof)+import Data.Map (fromList)+import qualified Data.Set as S+import Data.String (IsString)+import Test.HUnit++tests :: (FirstOrderFormula formula term v p f, N.Literal formula term v p f, Eq term, Show term, Show formula, Show v) =>+         [TestFormula formula term v p f] -> [TestProof formula term v] -> Test+tests fs ps =+    TestLabel "New" $ TestList (map doTest fs ++ map doProof ps)++allFormulas :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, Typeable formula, IsString v, IsString p, IsString f) =>+               [TestFormula formula term v p f]+allFormulas = (formulas +++               concatMap snd [animalKB, chang43KB] +++               animalConjectures +++               [chang43Conjecture, chang43ConjectureRenamed])++formulas :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+            [TestFormula formula term v p f]+formulas =+    let n = (.~.) :: Logic formula => formula -> formula+        p = pApp "p" :: [term] -> formula+        q = pApp "q" :: [term] -> formula+        r = pApp "r" :: [term] -> formula+        s = pApp "s" :: [term] -> formula+        t = pApp "t" :: [term] -> formula+        p0 = p [] :: formula+        q0 = q [] :: formula+        r0 = r [] :: formula+        s0 = s [] :: formula+        t0 = t [] :: formula+        (x, y, z, u, v, w) :: (term, term, term, term, term, term) =+                              (var "x", var "y", var "z", var "u", var "v", var "w") in+    [ +      TestFormula+      { formula = p0 .|. q0 .&. r0 .|. n s0 .&. n t0+      , name = "operator precedence"+      , expected = [ FirstOrderFormula ((p0 .|. q0) .&. (r0 .|. (n s0)) .&. (n t0)) ] }+    , TestFormula+      { formula = pApp (fromBool True) []+      , name = "True"+      , expected = [ClauseNormalForm  (toSS [[]])] }+    , TestFormula+      { formula = pApp (fromBool False) []+      , name = "False"+      , expected = [ClauseNormalForm  (toSS [])] }+    , TestFormula+      { formula = pApp "p" []+      , name = "p"+      , expected = [ClauseNormalForm  (toSS [[pApp "p" []]])] }+    , let p = pApp "p" [] in+      TestFormula+      { formula = p .&. ((.~.) (p))+      , name = "p&~p"+      , expected = [ PrenexNormalForm ((pApp ("p") []) .&. (((.~.) (pApp ("p") []))))+                   , ClauseNormalForm (toSS [[(p)], [((.~.) (p))]])+                   ] }+    , TestFormula+      { formula = pApp "p" [var "x"]+      , name = "p[x]"+      , expected = [ClauseNormalForm  (toSS [[pApp "p" [x]]])] }+    , let f = pApp "f"+          q = pApp "q" in+      TestFormula+      { name = "iff"+      , formula = for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))+      , expected = [ PrenexNormalForm +                     (for_all "x"+                      (for_all "y"+                       (for_all "z"+                        (exists "z2"+                         ((q [x,y] .&.+                           ((f [z,x] .&. f [z,y]) .|.+                            ((((.~.) (f [z,x])) .&. ((.~.) (f [z,y])))))) .|. ((((.~.) (q [x,y])) .&.+                            ((((f [var ("z2"),x] .&. (((.~.) (f [var ("z2"),y])))) .|.+                               (((.~.) (f [var ("z2"),x])))) .&. f [var ("z2"),y])))))+                        ))))+                   , ClauseNormalForm ++--                    [[((.~.) (q [var "x",var "y"])),+--                      ((.~.) (f [var "z",var "x"])),+--                      (f [var "z",var "y"])],+--                     [((.~.) (q [var "x",var "y"])),+--                      ((.~.) (f [var "z",var "y"])),+--                      (f [var "z",var "x"])],+--                     [(f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"]),+--                      (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"]),+--                      (q [var "x",var "y"])],+--                     [((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"])),+--                      (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"]),+--                      (q [var "x",var "y"])],+--                     [(f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"]),+--                      ((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"])),+--                      (q [var "x",var "y"])],+--                     [((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "y"])),+--                      ((.~.) (f [fApp (toSkolem 1) [var "x",var "y",var "z"],var "x"])),+--                      (q [var "x",var "y"])]]]++                     (toSS [[(f [var ("z"),var ("x")]),+                             (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+                             ((.~.) (f [var ("z"),var ("y")]))],+                            [(f [var ("z"),var ("x")]),+                             ((.~.) (f [var ("z"),var ("y")])),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))],+                            [(f [var ("z"),var ("x")]),+                             ((.~.) (f [var ("z"),var ("y")])),+                             ((.~.) (q [var ("x"),var ("y")]))],+                            [(f [var ("z"),var ("y")]),+                             (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+                             ((.~.) (f [var ("z"),var ("x")]))],+                            [(f [var ("z"),var ("y")]),+                             ((.~.) (f [var ("z"),var ("x")])),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))],+                            [(f [var ("z"),var ("y")]),+                             ((.~.) (f [var ("z"),var ("x")])),+                             ((.~.) (q [var ("x"),var ("y")]))],+                            [(f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]),+                             (q [var ("x"),var ("y")])],+                            [(q [var ("x"),var ("y")]),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("x")])),+                             ((.~.) (f [fApp (toSkolem 1) [var ("x"),var ("y")],var ("y")]))]])+                   ]+      }+    , TestFormula+      { name = "move quantifiers out"+      , formula = (for_all "x" (pApp "p" [x]) .&. (pApp "q" [x]))+      , expected = [PrenexNormalForm (for_all "x2" ((pApp "p" [var ("x2")]) .&. ((pApp "q" [var ("x")]))))]+      }+    , TestFormula+      { name = "skolemize2"+      , formula = exists "x" (for_all "y" (pApp "loves" [x, y]))+      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem 1) [],y])]+      }+    , TestFormula+      { name = "skolemize3"+      , formula = for_all "y" (exists "x" (pApp "loves" [x, y]))+      , expected = [SkolemNormalForm (pApp ("loves") [fApp (toSkolem 1) [y],y])]+      }+    , TestFormula+      { formula = exists "x" (for_all' ["y", "z"]+                              (exists "u"+                               (for_all "v"+                                (exists "w"+                                 (pApp "P" [x, y, z, u, v, w])))))+      , name = "chang example 4.1"+      , expected = [ SkolemNormalForm (pApp "P" [fApp (toSkolem 1) [],+                                                 var ("y"),+                                                 var ("z"),+                                                 fApp (toSkolem 2) [var ("y"),var ("z")],+                                                 var ("v"),+                                                 fApp (toSkolem 3) [var ("v"), var ("y"),var ("z")]]) ]+      }+    , TestFormula+      { name = "chang example 4.2"+      -- ∀x ∃y∃z ~P(x,y) & Q(x,z) | R(x,y,z)+      , formula = for_all "x" (exists' ["y", "z"] (((((.~.) (pApp "P" [x, y])) .&. pApp "Q" [x, z]) .|. pApp "R" [x, y, z])))+      -- ∀x ~P(x,Sk1[x]) | R(x,Sk1[x],Sk2[x]) & Q(x,Sk2[x]) | R(x,Sk1[x],Sk2[x])+      , expected = [ SkolemNormalForm+                     ((((.~.) (pApp ("P") [var ("x"),var ("y")])) .&.+                       ((pApp ("Q") [var ("x"),var ("z")]))) .|.+                      ((pApp ("R") [var ("x"),var ("y"),var ("z")])))+                   , ClauseNormalForm+                     (toSS +                      [[((.~.) (pApp ("P") [var ("x"),var ("y")])),+                       (pApp ("R") [var ("x"),var ("y"),var ("z")])],+                      [(pApp ("Q") [var ("x"),var ("z")]),+                       (pApp ("R") [var ("x"),var ("y"),var ("z")])]]) ]+      }+    , TestFormula+      { formula = n p0 .|. q0 .&. p0 .|. r0 .&. n q0 .&. n r0+      , name = "chang 7.2.1a - unsat"+      , expected = [ SatSolverSat False ] }+    , TestFormula+      { formula = p0 .|. q0 .|. r0 .&. n p0 .&. n q0 .&. n r0 .|. s0 .&. n s0+      , name = "chang 7.2.1b - unsat"+      , expected = [ SatSolverSat False ] }+    , TestFormula+      { formula = p0 .|. q0 .&. q0 .|. r0 .&. r0 .|. s0 .&. n r0 .|. n p0 .&. n s0 .|. n q0 .&. n q0 .|. n r0+      , name = "chang 7.2.1c - unsat"+      , expected = [ SatSolverSat False ] }+    , let q = pApp "q"+          f = pApp "f"+          sk1 = f [fApp (toSkolem 1) [x,x,y,z],y]+          sk2 = f [fApp (toSkolem 1) [x,x,y,z],x]+          (x, y, z) = (var "x", var "y", var "z") in+      TestFormula+      { name = "distribute bug test"+      , formula = ((((.~.) (q [x,y])) .|.+                    ((((.~.) (sk2)) .|. (sk1)) .&.+                     (((.~.) (sk1)) .|. (sk2)))) .&.+                   ((((sk2) .&.+                      ((.~.) (sk1))) .|. ((sk1) .&.+                      ((.~.) (sk2)))) .|. (q [x,y])))+      , expected = [ClauseNormalForm+                    (toSS+                     [[sk2,sk1,pApp ("q") [x,y]],+                      [sk2,((.~.) (sk1)),((.~.) (q [x,y]))],+                      [sk1,((.~.) (sk2)),((.~.) (q [x,y]))],+                      [q [x,y], ((.~.) sk2),((.~.) sk1)]])]+      }+    , let (x, y) = (var "x", var "y")+          (x', y') = (var "x", var "y") in+      TestFormula+      { name = "convert to Chiou 1"+      , formula = exists "x" (x .=. y)+      , expected = [ConvertToChiou (exists "x" (x' .=. y'))]+      }+    , let s = pApp "s"+          s' = pApp "s"+          x' = var "x"+          y' = var "y" in+      TestFormula+      { name = "convert to Chiou 2"+      , formula = s [fApp ("a") [x, y]]+      , expected = [ConvertToChiou (s' [fApp "a" [x', y']])]+      }+    , let s :: [term] -> formula+          s = pApp "s"+          h :: [term] -> formula+          h = pApp "h"+          m :: [term] -> formula+          m = pApp "m"+          s' :: [term] -> formula+          s' = pApp "s"+          h' :: [term] -> formula+          h' = pApp "h"+          m' :: [term] -> formula+          m' = pApp "m"+          x' :: term+          x' = var "x" in+      TestFormula+      { name = "convert to Chiou 3"+      , formula = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x]))+      , expected = [ConvertToChiou (for_all "x" (((s' [x'] .=>. h' [x']) .&. (h' [x'] .=>. m' [x'])) .=>. (s' [x'] .=>. m' [x'])))]+      }+    , let taller :: term -> term -> formula+          taller a b = pApp ("taller" :: p) [a, b]+          wise :: term -> formula+          wise a = pApp ("wise" :: p) [a] in+      TestFormula+      { name = "cnf test 1"+      , formula = for_all "y" (for_all "x" (taller y x .|. wise x) .=>. wise y)+      , expected = [ClauseNormalForm+                    (toSS+                     [[(pApp ("wise") [var ("y")]),+                       ((.~.) (pApp ("taller") [var ("y"),fApp (toSkolem 1) [var ("y")]]))],+                      [(pApp ("wise") [var ("y")]),+                       ((.~.) (pApp ("wise") [fApp (toSkolem 1) [var ("y")]]))]])]+      }+    , TestFormula+      { name = "cnf test 2"+      , formula = ((.~.) (exists "x" (pApp "s" [x] .&. pApp "q" [x])))+      , expected = [ ClauseNormalForm (toSS +                                       [[((.~.) (pApp ("q") [var ("x")])),+                                         ((.~.) (pApp ("s") [var ("x")]))]])+                   , PrenexNormalForm (for_all "x"+                                       (((.~.) (pApp ("s") [var ("x")])) .|.+                                        (((.~.) (pApp ("q") [var ("x")])))))+                                     {- [[((.~.) (pApp "s" [var "x"])),+                                        ((.~.) (pApp "q" [var "x"]))]] -}+                   ]+      }+    , TestFormula+      { name = "cnf test 3"+      , formula = (for_all "x" (p [x] .=>. (q [x] .|. r [x])))+      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [var "x"])),(pApp "q" [var "x"]),(pApp "r" [var "x"])]])]+      }+    , TestFormula+      { name = "cnf test 4"+      , formula = ((.~.) (exists "x" (p [x] .=>. exists "y" (q [y]))))+      , expected = [ClauseNormalForm (toSS [[(pApp "p" [var "x"])],[((.~.) (pApp "q" [var "y"]))]])]+      }+    , TestFormula+      { name = "cnf test 5"+      , formula = (for_all "x" (q [x] .|. r [x] .=>. s [x]))+      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "q" [var "x"])),(pApp "s" [var "x"])],[((.~.) (pApp "r" [var "x"])),(pApp "s" [var "x"])]])]+      }+    , TestFormula+      { name = "cnf test 6"+      , formula = (exists "x" (p0 .=>. pApp "f" [x]))+      , expected = [ClauseNormalForm (toSS [[((.~.) (pApp "p" [])),(pApp "f" [fApp (toSkolem 1) []])]])]+      }+    , let p = pApp "p" []+          f' = pApp "f" [x]+          f = pApp "f" [fApp (toSkolem 1) []] in+      TestFormula+      { name = "cnf test 7"+      , formula = exists "x" (p .<=>. f')+      , expected = [ PrenexNormalForm (exists "x" ((p .&. f') .|. ((((.~.) p) .&. (((.~.) f'))))))+                   , SkolemNormalForm ((p .&. f) .|. (((.~.) p) .&. (((.~.) f))))+                   , TrivialClauses [(False,S.fromList [((.~.) (pApp ("p") [])),(pApp ("f") [fApp (toSkolem 1) []])]),+                                     (False,S.fromList [((.~.) (pApp ("f") [fApp (toSkolem 1) []])),(pApp ("p") [])])]+                   , ClauseNormalForm (toSS [[(f), ((.~.) p)], [p, ((.~.) f)]])]+      }+    , TestFormula+      { name = "cnf test 8"+      , formula = (for_all "z" (exists "y" (for_all "x" (pApp "f" [x, y] .<=>. (pApp "f" [x, z] .&. ((.~.) (pApp "f" [x, x])))))))+      , expected = [ClauseNormalForm +                    (toSS [[((.~.) (pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])),(pApp "f" [var "x",var "z"])],+                           [((.~.) (pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])),((.~.) (pApp "f" [var "x",var "x"]))],+                           [((.~.) (pApp "f" [var "x",var "z"])),(pApp "f" [var "x",var "x"]),(pApp "f" [var "x",fApp (toSkolem 1) [var "z"]])]])]+      }+    , let f = pApp "f" +          q = pApp "q"+          sk1 = fApp (toSkolem 1)+          (x, y, z) = (var "x", var "y", var "z") in+      TestFormula+      { name = "cnf test 9"+      , formula = (for_all "x" (for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))))+      , expected = [ClauseNormalForm+                    (toSS+                     [[(f [z,x]),+                       (f [sk1 [x,y],y]),+                       ((.~.) (f [z,y]))],+                      [(f [z,x]),+                       ((.~.) (f [z,y])),+                       ((.~.) (f [sk1 [x,y],x])),+                       ((.~.) (f [sk1 [x,y],y]))],+                      [(f [z,x]),+                       ((.~.) (f [z,y])),+                       ((.~.) (q [x,y]))],+                      [(f [z,y]),+                       (f [sk1 [x,y],y]),+                       ((.~.) (f [z,x]))],+                      [(f [z,y]),+                       ((.~.) (f [z,x])),+                       ((.~.) (f [sk1 [x,y],x])),+                       ((.~.) (f [sk1 [x,y],y]))],+                      [(f [z,y]),+                       ((.~.) (f [z,x])),+                       ((.~.) (q [x,y]))],+                      [(f [sk1 [x,y],y]),+                       (q [x,y])],+                      [(q [x,y]),+                       ((.~.) (f [sk1 [x,y],x])),+                       ((.~.) (f [sk1 [x,y],y]))]])+                   ]+      }+    , TestFormula+      { name = "cnf test 10"+      , formula = (for_all "x" (exists "y" ((p [x, y] .<=. for_all "x" (exists "z" (q [y, x, z]) .=>. r [y])))))+      , expected = [ClauseNormalForm+                    (toSS +                     [[(pApp ("p") [var ("x"),fApp (toSkolem 1) [var ("x")]]),+                       (pApp ("q") [fApp (toSkolem 1) [fApp (toSkolem 2) []],fApp (toSkolem 2) [],fApp (toSkolem 3) []])],+                      [(pApp ("p") [var ("x"),fApp (toSkolem 1) [var ("x")]]),+                       ((.~.) (pApp ("r") [fApp (toSkolem 1) [fApp (toSkolem 2) []]]))]])+                   ]+      }+    , TestFormula+      { name = "cnf test 11"+      , formula = (for_all "x" (for_all "z" (p [x, z] .=>. exists "y" ((.~.) (q [x, y] .|. ((.~.) (r [y, z])))))))+      , expected = [ClauseNormalForm+                    (toSS +                    [[((.~.) (pApp "p" [var "x",var "z"])),((.~.) (pApp "q" [var "x",fApp (toSkolem 1) [var "x",var "z"]]))],+                     [((.~.) (pApp "p" [var "x",var "z"])),(pApp "r" [fApp (toSkolem 1) [var "x",var "z"],var "z"])]])]+      }+    , TestFormula+      { name = "cnf test 12"+      , formula = ((p0 .=>. q0) .=>. (((.~.) r0) .=>. (s0 .&. t0)))+      , expected = [ClauseNormalForm+                    (toSS+                    [[(pApp "p" []),(pApp "r" []),(pApp "s" [])],+                     [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "s" [])],+                     [(pApp "p" []),(pApp "r" []),(pApp "t" [])],+                     [((.~.) (pApp "q" [])),(pApp "r" []),(pApp "t" [])]])]+      }+    , let p = pApp "p" []+          true = pApp (fromBool True) []+          false = pApp (fromBool False) [] in+      TestFormula+      { name = "psimplify 50"+      , formula = true .=>. (p .<=>. (p .<=>. false))+      , expected = [ SimplifiedForm (p .<=>. (.~.) p) ] }+    , let true = pApp (fromBool True) []+          false = pApp (fromBool False) [] in+      TestFormula+      { name = "psimplify 51"+      , formula = (((pApp "x" [] .=>. pApp "y" []) .=>. true) .|. false)+      , expected = [ SimplifiedForm (pApp (fromBool True) []) ] }+    , let false = pApp (fromBool False) []+          q = pApp "q" [] in+      TestFormula+      { name = "simplify 140.3"+      , formula = (for_all "x"+                   (for_all "y"+                    (pApp "p" [var "x"] .|. (pApp "p" [var "y"] .&. false))) .=>.+                   (exists "z" q))+      , expected = [ SimplifiedForm ((for_all "x" (pApp "p" [var "x"])) .=>.+                                        (pApp "q" [])) ] }+    , TestFormula+      { name = "nnf 141.1"+      , formula = ((for_all "x" (pApp "p" [var "x"])) .=>. ((exists "y" (pApp "q" [var "y"])) .<=>. (exists "z" (pApp "p" [var "z"] .&. pApp "q" [var "z"]))))+      , expected = [ NegationNormalForm +                     ((exists "x" ((.~.) (pApp "p" [var "x"]))) .|.+                      ((((exists "y" (pApp "q" [var "y"])) .&. ((exists "z" ((pApp "p" [var "z"]) .&. ((pApp "q" [var "z"])))))) .|.+                        (((for_all "y" ((.~.) (pApp "q" [var "y"]))) .&.+                          ((for_all "z" (((.~.) (pApp "p" [var "z"])) .|. (((.~.) (pApp "q" [var "z"]))))))))))) ] }+    , TestFormula+      { name = "pnf 144.1"+      , formula = (for_all "x" (pApp "p" [var "x"] .|. pApp "r" [var "y"]) .=>.+                   (exists "y" (exists "z" (pApp "q" [var "y"] .|. ((.~.) (exists "z" (pApp "p" [var "z"] .&. pApp "q" [var "z"])))))))+      , expected = [ PrenexNormalForm +                     (exists "x" +                      (for_all "z"+                       ((((.~.) (pApp "p" [var "x"])) .&. (((.~.) (pApp "r" [var "y"])))) .|.+                        (((pApp "q" [var "x"]) .|. ((((.~.) (pApp "p" [var "z"])) .|. (((.~.) (pApp "q" [var "z"])))))))))) ] }+    , let (x, y, u, v) = (var "x", var "y", var "u", var "v")+          fv = fApp (toSkolem 2) [u,x]+          fy = fApp (toSkolem 1) [x] in+      TestFormula+      { name = "snf 150.1"+      , formula = (exists "y" (pApp "<" [x, y] .=>. for_all "u" (exists "v" (pApp "<" [fApp "*" [x, u], fApp "*" [y, v]]))))+      , expected = [ SkolemNormalForm (((.~.) (pApp "<" [x, fy])) .|. pApp "<" [fApp "*" [x, u], fApp "*" [fy, fv]]) ] }+    , let p x = pApp "p" [x]+          q x = pApp "q" [x]+          (x, y, z) = (var "x", var "y", var "z") in+      TestFormula+      { name = "snf 150.2"+      , formula = (for_all "x" (p x .=>. (exists "y" (exists "z" (q y .|. (.~.) (exists "z" (p z .&. (q z))))))))+      , expected = [ SkolemNormalForm (((.~.) (p x)) .|. (q (fApp (toSkolem 1) []) .|. (((.~.) (p z)) .|. ((.~.) (q z))))) ] }+    ]++animalKB :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+            (String, [TestFormula formula term v p f])+animalKB =+    let x = var "x"+        y = var "y"+        dog = pApp "Dog"+        cat = pApp "Cat"+        owns = pApp "Owns"+        kills = pApp "Kills"+        animal = pApp "Animal"+        animalLover = pApp "AnimalLover"+        jack = fApp "Jack" []+        tuna = fApp "Tuna" []+        curiosity = fApp "Curiosity" [] in+    ("animal"+    , [ TestFormula+       { formula = exists "x" (dog [x] .&. owns [jack, x]) -- [[Pos 1],[Pos 2]]+       , name = "jack owns a dog"+       , expected = [ClauseNormalForm (toSS [[(pApp "Dog" [fApp (toSkolem 1) []])],[(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])]])]+       -- owns(jack,sK0)+       -- dog (SK0)+                   }+     , TestFormula+       { formula = for_all "x" ((exists "y" (dog [y] .&. (owns [x, y]))) .=>. (animalLover [x])) -- [[Neg 1,Neg 2,Pos 3]]+       , name = "dog owners are animal lovers"+       , expected = [ PrenexNormalForm (for_all "x" (for_all "y" ((((.~.) (pApp "Dog" [var "y"])) .|.+                                                                           (((.~.) (pApp "Owns" [var "x",var "y"])))) .|.+                                                                          ((pApp "AnimalLover" [var "x"])))))+                    , ClauseNormalForm (toSS [[((.~.) (pApp "Dog" [var "y"])),((.~.) (pApp "Owns" [var "x",var "y"])),(pApp "AnimalLover" [var "x"])]]) ]+       -- animalLover(X0) | ~owns(X0,sK1(X0)) | ~dog(sK1(X0))+       }+     , TestFormula+       { formula = for_all "x" (animalLover [x] .=>. (for_all "y" ((animal [y]) .=>. ((.~.) (kills [x, y]))))) -- [[Neg 3,Neg 4,Neg 5]]+       , name = "animal lovers don't kill animals"+       , expected = [ClauseNormalForm  (toSS [[((.~.) (pApp "AnimalLover" [var "x"])),((.~.) (pApp "Animal" [var "y"])),((.~.) (pApp "Kills" [var "x",var "y"]))]])]+       -- ~kills(X0,X2) | ~animal(X2) | ~animalLover(sK2(X0))+       }+     , TestFormula+       { formula = (kills [jack, tuna]) .|. (kills [curiosity, tuna]) -- [[Pos 5,Pos 5]]+       , name = "Either jack or curiosity kills tuna"+       , expected = [ClauseNormalForm  (toSS [[(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])]])]+       -- kills(curiosity,tuna) | kills(jack,tuna)+       }+     , TestFormula+       { formula = cat [tuna] -- [[Pos 6]]+       , name = "tuna is a cat"+       , expected = [ClauseNormalForm  (toSS [[(pApp "Cat" [fApp "Tuna" []])]])]+       -- cat(tuna)+       }+     , TestFormula+       { formula = for_all "x" ((cat [x]) .=>. (animal [x])) -- [[Neg 6,Pos 4]]+       , name = "a cat is an animal"+       , expected = [ClauseNormalForm  (toSS [[((.~.) (pApp "Cat" [var "x"])),(pApp "Animal" [var "x"])]])]+       -- animal(X0) | ~cat(X0)+       }+     ])++animalConjectures :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+                     [TestFormula formula term v p f]+animalConjectures =+    let kills = pApp "Kills" :: [term] -> formula+        jack = fApp "Jack" [] :: term+        tuna = fApp "Tuna" [] :: term+        curiosity = fApp "Curiosity" [] :: term in++    map (withKB animalKB) $+     [ TestFormula+       { formula = kills [jack, tuna]             -- False+       , name = "jack kills tuna"+       , expected =+           [ FirstOrderFormula ((.~.) (((exists "x" ((pApp "Dog" [var ("x")]) .&. ((pApp "Owns" [fApp ("Jack") [],var ("x")])))) .&.+                                        (((for_all "x" ((exists "y" ((pApp "Dog" [var ("y")]) .&. ((pApp "Owns" [var ("x"),var ("y")])))) .=>.+                                                          ((pApp "AnimalLover" [var ("x")])))) .&.+                                          (((for_all "x" ((pApp "AnimalLover" [var ("x")]) .=>.+                                                            ((for_all "y" ((pApp "Animal" [var ("y")]) .=>.+                                                                             (((.~.) (pApp "Kills" [var ("x"),var ("y")])))))))) .&.+                                            ((((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]) .|. ((pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.+                                              (((pApp "Cat" [fApp ("Tuna") []]) .&.+                                                ((for_all "x" ((pApp "Cat" [var ("x")]) .=>.+                                                                 ((pApp "Animal" [var ("x")])))))))))))))) .=>.+                                       ((pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]))))++           , PrenexNormalForm+             (for_all "x"+              (for_all "y"+               (exists "x2"+                ((((pApp ("Dog") [var ("x2")]) .&.+                   ((pApp ("Owns") [fApp ("Jack") [],var ("x2")]))) .&.+                  ((((((.~.) (pApp ("Dog") [var ("y")])) .|.+                      (((.~.) (pApp ("Owns") [var ("x"),var ("y")])))) .|.+                     ((pApp ("AnimalLover") [var ("x")]))) .&.+                    (((((.~.) (pApp ("AnimalLover") [var ("x")])) .|.+                       ((((.~.) (pApp ("Animal") [var ("y")])) .|.+                         (((.~.) (pApp ("Kills") [var ("x"),var ("y")])))))) .&.+                      ((((pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]) .|.+                         ((pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]))) .&.+                        (((pApp ("Cat") [fApp ("Tuna") []]) .&.+                          ((((.~.) (pApp ("Cat") [var ("x")])) .|.+                            ((pApp ("Animal") [var ("x")]))))))))))))) .&.+                 (((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])))))))+           , ClauseNormalForm+             (toSS+              [[(pApp ("Animal") [var ("x")]),+                ((.~.) (pApp ("Cat") [var ("x")]))],+               [(pApp ("AnimalLover") [var ("x")]),+                ((.~.) (pApp ("Dog") [var ("y")])),+                ((.~.) (pApp ("Owns") [var ("x"),var ("y")]))],+               [(pApp ("Cat") [fApp ("Tuna") []])],+               [(pApp ("Dog") [fApp (toSkolem 1) []])],+               [(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),+                (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])],+               [(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])],+               [((.~.) (pApp ("Animal") [var ("y")])),+                ((.~.) (pApp ("AnimalLover") [var ("x")])),+                ((.~.) (pApp ("Kills") [var ("x"),var ("y")]))],+               [((.~.) (pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []]))]])+           , ChiouKB1+             (Proof+              Invalid+              (S.fromList +               [makeINF' ([]) ([(pApp ("Cat") [fApp ("Tuna") []])]),+                makeINF' ([]) ([(pApp ("Dog") [fApp (toSkolem 1) []])]),+                makeINF' ([]) ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []]),(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),+                makeINF' ([]) ([(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]),+                makeINF' ([(pApp ("Animal") [var ("y")]),(pApp ("AnimalLover") [var ("x")]),(pApp ("Kills") [var ("x"),var ("y")])]) ([]),+                makeINF' ([(pApp ("Cat") [var ("x")])]) ([(pApp ("Animal") [var ("x")])]),+                makeINF' ([(pApp ("Dog") [var ("y")]),(pApp ("Owns") [var ("x"),var ("y")])]) ([(pApp ("AnimalLover") [var ("x")])]),+                makeINF' ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]) ([])]))+           ]+       }+     , TestFormula+       { formula = kills [curiosity, tuna]        -- True+       , name = "curiosity kills tuna"+       , expected =+           [ ClauseNormalForm+             (toSS+             [[(pApp "Dog" [fApp (toSkolem 1) []])],+              [(pApp "Owns" [fApp ("Jack") [],fApp (toSkolem 1) []])],+              [((.~.) (pApp "Dog" [var ("y")])),+               ((.~.) (pApp "Owns" [var ("x"),var ("y")])),+               (pApp "AnimalLover" [var ("x")])],+              [((.~.) (pApp "AnimalLover" [var ("x")])),+               ((.~.) (pApp "Animal" [var ("y")])),+               ((.~.) (pApp "Kills" [var ("x"),var ("y")]))],+              [(pApp "Kills" [fApp ("Jack") [],fApp ("Tuna") []]),+               (pApp "Kills" [fApp ("Curiosity") [],fApp ("Tuna") []])],+              [(pApp "Cat" [fApp ("Tuna") []])],+              [((.~.) (pApp "Cat" [var ("x")])),+               (pApp "Animal" [var ("x")])],+              [((.~.) (pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]))]])+           , PropLogicSat True+{-+           , SatSolverCNF [ [Neg 1,Neg 2,Neg 3]    -- animallover(x)|animal(y)|kills(x,y)+                          , [Neg 4,Pos 5]          -- ~cat(x)|animal(x)+                          , [Neg 6,Neg 7,Pos 2]    -- ~dog(y)|~owns(x,y)|animallover(x)+                          , [Neg 8]                -- ~kills(curisity,tuna)+                          , [Pos 8,Pos 11]         -- kills(curiosity,tuna)|kills(jack,tuna)+                          , [Pos 9]                -- cat(tuna)+                          , [Pos 10]               -- owns(jack,sk1)+                          , [Pos 12]               -- dog(sk1)+                          ]+-}+           -- I haven't tried to figure out if this is correct, it+           -- probably is because things are working.+           , SatSolverCNF [[Neg 2,Pos 1],[Neg 3,Neg 11,Neg 12],[Neg 4,Neg 5,Pos 3],[Neg 8],[Pos 6],[Pos 7],[Pos 8,Pos 9],[Pos 10]]+           -- It seems like this should be True.+           , SatSolverSat False+           ]+       }+     ]++socratesKB =+    let x = var "x"+        socrates x = pApp "Socrates" [x]+        human x = pApp "Human" [x]+        mortal x = pApp "Mortal" [x] in+    ("socrates"+    , [ TestFormula+       { name = "all humans are mortal"+       , formula = for_all "x" (human x .=>. mortal x)+       , expected = [ClauseNormalForm  (toSS [[((.~.) (human x)), mortal x]])] }+     , TestFormula+       { name = "socrates is human"+       , formula = for_all "x" (socrates x .=>. human x)+       , expected = [ClauseNormalForm  (toSS [[(.~.) (socrates x), human x]])] }+     ])++{-+socratesConjectures =+    map (withKB socratesKB)+     [ TestFormula+       { formula = for_all' [V "x"] (socrates x .=>. mortal x)+       , name = "socrates is mortal"+       , expected = [ FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))) .&.+                                                 ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Human" [var "x"])))))) .=>.+                                                ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))))))+                    , ClauseNormalForm  [[((.~.) (pApp "Human" [var "x2"])),(pApp "Mortal" [var "x2"])],+                                          [((.~.) (pApp "Socrates" [var "x2"])),(pApp "Human" [var "x2"])],+                                          [(pApp "Socrates" [fApp (toSkolem 1) [var "x2",var "x2"]])],+                                          [((.~.) (pApp "Mortal" [fApp (toSkolem 1) [var "x2",var "x2"]]))]]+                    , SatPropLogic True ]+       }+     , TestFormula+       { formula = (.~.) (for_all' [V "x"] (socrates x .=>. mortal x))+       , name = "not (socrates is mortal)"+       , expected = [ SatPropLogic False+                    , FirstOrderFormula ((.~.) (((for_all' [V "x"] ((pApp "Human" [var "x"]) .=>. ((pApp "Mortal" [var "x"])))) .&.+                                                 ((for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Human" [var "x"])))))) .=>.+                                                (((.~.) (for_all' [V "x"] ((pApp "Socrates" [var "x"]) .=>. ((pApp "Mortal" [var "x"]))))))))+                    -- [~human(x) | mortal(x)], [~socrates(Sk1(x,y)) | human(Sk1(x,y))], socrates(Sk1(x,y)), ~mortal(Sk1(x,y))+                    -- ~1 | 2, ~3 | 4, 3, ~5?+                    , ClauseNormalForm [[((.~.) (pApp "Human" [x])), (pApp "Mortal" [x])],+                                         [((.~.) (pApp "Socrates" [fApp (toSkolem 1) [x,y]])), (pApp "Human" [fApp (toSkolem 1) [x,y]])],+                                         [(pApp "Socrates" [fApp (toSkolem 1) [x,y]])], [((.~.) (pApp "Mortal" [fApp (toSkolem 1) [x,y]]))]]+                    , ClauseNormalForm [[((.~.) (pApp "Human" [var "x2"])), (pApp "Mortal" [var "x2"])],+                                         [((.~.) (pApp "Socrates" [var "x2"])), (pApp "Human" [var "x2"])],+                                         [((.~.) (pApp "Socrates" [var "x"])), (pApp "Mortal" [var "x"])]] ]+       }+     ]+-}++chang43KB = +    let e = fApp "e" []+        (x, y, z, u, v, w) = (var "x", var "y", var "z", var "u", var "v", var "w") in+    ("chang example 4.3"+    , [ TestFormula { name = "closure property"+                    , formula = for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z]))+                    , expected = [] }+      , TestFormula { name = "associativity property"+                    , formula = for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [u, z, w] .=>. pApp "P" [x, v, w]) .&.+                                for_all' ["x", "y", "z", "u", "v", "w"] (pApp "P" [x, y, u] .&. pApp "P" [y, z, v] .&. pApp "P" [x, v, w] .=>. pApp "P" [u, z, w])+                    , expected = [] }+      , TestFormula { name = "identity property"+                    , formula = (for_all "x" (pApp "P" [x,e,x])) .&. (for_all "x" (pApp "P" [e,x,x]))+                    , expected = [] }+      , TestFormula { name = "inverse property"+                    , formula = (for_all "x" (pApp "P" [x,fApp "i" [x], e])) .&. (for_all "x" (pApp "P" [fApp "i" [x], x, e]))+                    , expected = [] }+      ])++chang43Conjecture :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+                     TestFormula formula term v p f+chang43Conjecture =+    let e = (fApp "e" [])+        (x, u, v, w) = (var "x", var "u", var "v", var "w") in+    withKB chang43KB $+    TestFormula { name = "G is commutative"+                , formula = for_all "x" (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w]))) +                , expected =+                    [ FirstOrderFormula +                      ((.~.) (((for_all' ["x","y"] (exists "z" (pApp "P" [var ("x"),var ("y"),var ("z")]))) .&. ((((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [var ("x"),var ("y"),var ("u")]) .&. ((pApp "P" [var ("y"),var ("z"),var ("v")]))) .&. ((pApp "P" [var ("u"),var ("z"),var ("w")]))) .=>. ((pApp "P" [var ("x"),var ("v"),var ("w")])))) .&. ((for_all' ["x","y","z","u","v","w"] ((((pApp "P" [var ("x"),var ("y"),var ("u")]) .&. ((pApp "P" [var ("y"),var ("z"),var ("v")]))) .&. ((pApp "P" [var ("x"),var ("v"),var ("w")]))) .=>. ((pApp "P" [var ("u"),var ("z"),var ("w")])))))) .&. ((((for_all "x" (pApp "P" [var ("x"),fApp ("e") [],var ("x")])) .&. ((for_all "x" (pApp "P" [fApp ("e") [],var ("x"),var ("x")])))) .&. (((for_all "x" (pApp "P" [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])) .&. ((for_all "x" (pApp "P" [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])))))))))) .=>. ((for_all "x" ((pApp "P" [var ("x"),var ("x"),fApp ("e") []]) .=>. ((for_all' ["u","v","w"] ((pApp "P" [var ("u"),var ("v"),var ("w")]) .=>. ((pApp "P" [var ("v"),var ("u"),var ("w")]))))))))))+                      -- (∀x ∀y ∃z P(x,y,z)) &+                      -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(u,z,w) | P(x,v,w)) &+                      -- (∀x∀y∀z∀u∀v∀w ~P(x,y,u) | ~P(y,z,v) | ~P(x,v,w) | P(u,z,w)) &+                      -- (∀x P(x,e,x)) &+                      -- (∀x P(e,x,x)) &+                      -- (∀x P(x,i[x],e)) &+                      -- (∀x P(i[x],x,e)) &+                      -- (∃x P(x,x,e) & (∃u∃v∃w P(u,v,w) & ~P(v,u,w)))+                    , NegationNormalForm+                      (((for_all "x"+                         (for_all "y"+                          (exists "z"+                           (pApp ("P") [var ("x"),var ("y"),var ("z")])))) .&.+                        ((((for_all "x"+                            (for_all "y"+                             (for_all "z"+                              (for_all "u"+                               (for_all "v"+                                (for_all "w"+                                 (((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                                    (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                                   (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+                                  ((pApp ("P") [var ("x"),var ("v"),var ("w")]))))))))) .&.+                           ((for_all "x"+                             (for_all "y"+                              (for_all "z"+                               (for_all "u"+                                (for_all "v"+                                 (for_all "w"+                                  (((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                                     (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                                    (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+                                   ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))))))))) .&.+                          ((((for_all "x" (pApp ("P") [var ("x"),fApp ("e") [],var ("x")])) .&.+                             ((for_all "x" (pApp ("P") [fApp ("e") [],var ("x"),var ("x")])))) .&.+                            (((for_all "x" (pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])) .&.+                              ((for_all "x" (pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])))))))))) .&.+                       ((exists "x"+                         ((pApp ("P") [var ("x"),var ("x"),fApp ("e") []]) .&.+                          ((exists "u"+                            (exists "v"+                             (exists "w"+                              ((pApp ("P") [var ("u"),var ("v"),var ("w")]) .&.+                               (((.~.) (pApp ("P") [var ("v"),var ("u"),var ("w")]))))))))))))+                    , PrenexNormalForm+                      (for_all "x"+                       (for_all "y"+                        (for_all "z"+                         (for_all "u"+                          (for_all "v"+                           (for_all "w"+                            (exists "z2"+                             (exists "x2"+                              (exists "u2"+                               (exists "v2"+                                (exists "w2"+                                 (((pApp ("P") [var ("x"),var ("y"),var ("z2")]) .&.+                                   ((((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                                         (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                                        (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+                                       ((pApp ("P") [var ("x"),var ("v"),var ("w")]))) .&.+                                      ((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                                          (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                                         (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+                                        ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))) .&.+                                     ((((pApp ("P") [var ("x"),fApp ("e") [],var ("x")]) .&.+                                        ((pApp ("P") [fApp ("e") [],var ("x"),var ("x")]))) .&.+                                       (((pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []]) .&.+                                         ((pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []]))))))))) .&.+                                  (((pApp ("P") [var ("x2"),var ("x2"),fApp ("e") []]) .&.+                                    (((pApp ("P") [var ("u2"),var ("v2"),var ("w2")]) .&.+                                      (((.~.) (pApp ("P") [var ("v2"),var ("u2"),var ("w2")])))))))))))))))))))+                    , SkolemNormalForm+                      (((pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]]) .&.+                        ((((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                              (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                             (((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])))) .|.+                            ((pApp ("P") [var ("x"),var ("v"),var ("w")]))) .&.+                           ((((((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])) .|.+                               (((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])))) .|.+                              (((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])))) .|.+                             ((pApp ("P") [var ("u"),var ("z"),var ("w")]))))) .&.+                          ((((pApp ("P") [var ("x"),fApp ("e") [],var ("x")]) .&.+                             ((pApp ("P") [fApp ("e") [],var ("x"),var ("x")]))) .&.+                            (((pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []]) .&.+                              ((pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []]))))))))) .&.+                       (((pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []]) .&.+                         (((pApp ("P") [fApp (toSkolem 3) [],fApp (toSkolem 4) [],fApp (toSkolem 5) []]) .&.+                           (((.~.) (pApp ("P") [fApp (toSkolem 4) [],fApp (toSkolem 3) [],fApp (toSkolem 5) []]))))))))+                    , SkolemNumbers (S.fromList [1,2,3,4,5])+                    -- From our algorithm++                    , ClauseNormalForm+                      (toSS +                      [[(pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]])],+                       [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+                        ((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])),+                        ((.~.) (pApp ("P") [var ("u"),var ("z"),var ("w")])),+                        (pApp ("P") [var ("x"),var ("v"),var ("w")])],+                       [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+                        ((.~.) (pApp ("P") [var ("y"),var ("z"),var ("v")])),+                        ((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])),+                        (pApp ("P") [var ("u"),var ("z"),var ("w")])],+                       [(pApp ("P") [var ("x"),fApp ("e") [],var ("x")])],+                       [(pApp ("P") [fApp ("e") [],var ("x"),var ("x")])],+                       [(pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])],+                       [(pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])],+                       [(pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []])],+                       [(pApp ("P") [fApp (toSkolem 3) [],fApp (toSkolem 4) [],fApp (toSkolem 5) []])],+                       [((.~.) (pApp ("P") [fApp (toSkolem 4) [],fApp (toSkolem 3) [],fApp (toSkolem 5) []]))]])++                    -- From the book+{-+                    , let (a, b, c) = +                              (fApp (toSkolem 3) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")],+                               fApp (toSkolem 4) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")],+                               fApp (toSkolem 5) [var ("x"),var ("y"),var ("x2"),var ("y2"),var ("z2"),var ("u"),var ("v"),var ("w"),var ("x2"),var ("y2"),var ("z2"),var ("u2"),var ("v2"),var ("w2"),var ("x3"),var ("x3"),var ("x3"),var ("x3")]) in+                      ClauseNormalForm+                      [[(pApp "P" [var "x",var "y",fApp (toSkolem 1) [var "x",var "y"]])],+                       [((.~.) (pApp "P" [var "x",var "y",var "u"])),+                        ((.~.) (pApp "P" [var "y",var "z",var "v"])),+                        ((.~.) (pApp "P" [var "u",var "z",var "w"])),+                        (pApp "P" [var "x",var "v",var "w"])],+                       [((.~.) (pApp "P" [var "x",var "y",var "u"])),+                        ((.~.) (pApp "P" [var "y",var "z",var "v"])),+                        ((.~.) (pApp "P" [var "x",var "v",var "w"])),+                        (pApp "P" [var "u",var "z",var "w"])],+                       [(pApp "P" [var "x",fApp "e" [],var "x"])],+                       [(pApp "P" [fApp "e" [],var "x",var "x"])],+                       [(pApp "P" [var "x",fApp "i" [var "x"],fApp "e" []])],+                       [(pApp "P" [fApp "i" [var "x"],var "x",fApp "e" []])],+                       [(pApp "P" [var "x",+                                   var "x",+                                   fApp "e" []])],+                       [(pApp "P" [a, b, c])],+                       [((.~.) (pApp "P" [b, a, c]))]]+-}+                    ]+                }++{-+% ghci+> :load Test/Data.hs+> :m +Logic.FirstOrder+> :m +Logic.Normal+> let f = (.~.) (conj (map formula (snd chang43KB)) .=>. formula chang43Conjecture)+> putStrLn (runNormal (cnfTrace f))+-}++chang43ConjectureRenamed :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+                            TestFormula formula term v p f+chang43ConjectureRenamed =+    let e = fApp "e" []+        (x, y, z, u, v, w) = (var "x", var "y", var "z", var "u", var "v", var "w")+        (u2, v2, w2, x2, y2, z2, u3, v3, w3, x3, y3, z3, x4, x5, x6, x7, x8) =+            (var "u2", var "v2", var "w2", var "x2", var "y2", var "z2", var "u3", var "v3", var "w3", var "x3", var "y3", var "z3", var "x4", var "x5", var "x6", var "x7", var "x8") in+    TestFormula { name = "chang 43 renamed"+                , formula = (.~.) ((for_all' ["x", "y"] (exists "z" (pApp "P" [x,y,z])) .&.+                                    for_all' ["x2", "y2", "z2", "u", "v", "w"] (pApp "P" [x2, y2, u] .&. pApp "P" [y2, z2, v] .&. pApp "P" [u, z2, w] .=>. pApp "P" [x2, v, w]) .&.+                                    for_all' ["x3", "y3", "z3", "u2", "v2", "w2"] (pApp "P" [x3, y3, u2] .&. pApp "P" [y3, z3, v2] .&. pApp "P" [x3, v2, w2] .=>. pApp "P" [u2, z3, w2]) .&.+                                    for_all "x4" (pApp "P" [x4,e,x4]) .&.+                                    for_all "x5" (pApp "P" [e,x5,x5]) .&.+                                    for_all "x6" (pApp "P" [x6,fApp "i" [x6], e]) .&.+                                    for_all "x7" (pApp "P" [fApp "i" [x7], x7, e])) .=>.+                                   (for_all "x8" (pApp "P" [x8, x8, e] .=>. (for_all' ["u3", "v3", "w3"] (pApp "P" [u3, v3, w3] .=>. pApp "P" [v3, u3, w3])))))+                , expected =+                    [ FirstOrderFormula+                      ((.~.) ((((((((for_all' ["x","y"] (exists "z" (pApp "P" [var "x",var "y",var "z"]))) .&.+                                    ((for_all' ["x2","y2","z2","u","v","w"] ((((pApp "P" [var "x2",var "y2",var "u"]) .&.+                                                                                          ((pApp "P" [var "y2",var "z2",var "v"]))) .&.+                                                                                         ((pApp "P" [var "u",var "z2",var "w"]))) .=>.+                                                                                        ((pApp "P" [var "x2",var "v",var "w"])))))) .&.+                                   ((for_all' ["x3","y3","z3","u2","v2","w2"] ((((pApp "P" [var "x3",var "y3",var "u2"]) .&.+                                                                                            ((pApp "P" [var "y3",var "z3",var "v2"]))) .&.+                                                                                           ((pApp "P" [var "x3",var "v2",var "w2"]))) .=>.+                                                                                          ((pApp "P" [var "u2",var "z3",var "w2"])))))) .&.+                                  ((for_all "x4" (pApp "P" [var "x4",fApp "e" [],var "x4"])))) .&.+                                 ((for_all "x5" (pApp "P" [fApp "e" [],var "x5",var "x5"])))) .&.+                                ((for_all "x6" (pApp "P" [var "x6",fApp "i" [var "x6"],fApp "e" []])))) .&.+                               ((for_all "x7" (pApp "P" [fApp "i" [var "x7"],var "x7",fApp "e" []])))) .=>.+                              ((for_all "x8" ((pApp "P" [var "x8",var "x8",fApp "e" []]) .=>.+                                                  ((for_all' ["u3","v3","w3"] ((pApp "P" [var "u3",var "v3",var "w3"]) .=>.+                                                                                    ((pApp "P" [var "v3",var "u3",var "w3"]))))))))))+                    , let a = fApp (toSkolem 3) []+                          b = fApp (toSkolem 4) []+                          c = fApp (toSkolem 5) [] in+                      ClauseNormalForm+                      (toSS+                      [[(pApp ("P") [var ("x"),var ("y"),fApp (toSkolem 1) [var ("x"),var ("y")]])],+                       [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+                        ((.~.) (pApp ("P") [var ("y"),var ("z2"),var ("v")])),+                        ((.~.) (pApp ("P") [var ("u"),var ("z2"),var ("w")])),+                        (pApp ("P") [var ("x"),var ("v"),var ("w")])],+                       [((.~.) (pApp ("P") [var ("x"),var ("y"),var ("u")])),+                        ((.~.) (pApp ("P") [var ("y"),var ("z2"),var ("v")])),+                        ((.~.) (pApp ("P") [var ("x"),var ("v"),var ("w")])),+                        (pApp ("P") [var ("u"),var ("z2"),var ("w")])],+                       [(pApp ("P") [var ("x"),fApp ("e") [],var ("x")])],+                       [(pApp ("P") [fApp ("e") [],var ("x"),var ("x")])],+                       [(pApp ("P") [var ("x"),fApp ("i") [var ("x")],fApp ("e") []])],+                       [(pApp ("P") [fApp ("i") [var ("x")],var ("x"),fApp ("e") []])],+                       [(pApp ("P") [fApp (toSkolem 2) [],fApp (toSkolem 2) [],fApp ("e") []])],+                       [(pApp ("P") [a,b,c])],+                       [((.~.) (pApp ("P") [b,a,c]))]])                      +                    ]+                }++withKB :: forall formula term v p f. (FirstOrderFormula formula term v p f) =>+          (String, [TestFormula formula term v p f]) -> TestFormula formula term v p f -> TestFormula formula term v p f+withKB (kbName, knowledge) conjecture =+    conjecture { name = name conjecture ++ " with " ++ kbName ++ " knowledge base"+               -- Here we say that the conjunction of the knowledge+               -- base formula implies the conjecture.  We prove the+               -- theorem by showing that the negation is+               -- unsatisfiable.+               , formula = (.~.) (conj (map formula knowledge) .=>. formula conjecture)}+    where+      conj [] = error "conj []"+      conj [x] = x+      conj (x:xs) = x .&. conj xs++kbKnowledge :: forall formula term v p f. (FirstOrderFormula formula term v p f) =>+               (String, [TestFormula formula term v p f]) -> (String, [formula])+kbKnowledge kb = (fst (kb :: (String, [TestFormula formula term v p f])), map formula (snd kb))++proofs :: forall formula term v p f. (FirstOrderFormula formula term v p f, Ord formula, IsString v, IsString p, IsString f) =>+          [TestProof formula term v]+proofs =+    let -- dog = pApp "Dog" :: [term] -> formula+        -- cat = pApp "Cat" :: [term] -> formula+        -- owns = pApp "Owns" :: [term] -> formula+        kills = pApp "Kills" :: [term] -> formula+        -- animal = pApp "Animal" :: [term] -> formula+        -- animalLover = pApp "AnimalLover" :: [term] -> formula+        socrates = pApp "Socrates" :: [term] -> formula+        -- human = pApp "Human" :: [term] -> formula+        mortal = pApp "Mortal" :: [term] -> formula++        jack :: term+        jack = fApp "Jack" []+        tuna :: term+        tuna = fApp "Tuna" []+        curiosity :: term+        curiosity = fApp "Curiosity" [] in++    [ TestProof+      { proofName = "prove jack kills tuna"+      , proofKnowledge = kbKnowledge (animalKB :: (String, [TestFormula formula term v p f]))+      , conjecture = kills [jack, tuna]+      , proofExpected = +          [ ChiouKB (S.fromList+                     [WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Dog" [fApp (toSkolem 1) []])]), wiIdent = 1},+                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])]), wiIdent = 1},+                      WithId {wiItem = INF (S.fromList [(pApp "Dog" [var "y"]),(pApp "Owns" [var "x",var "y"])]) (S.fromList [(pApp "AnimalLover" [var "x"])]), wiIdent = 2},+                      WithId {wiItem = INF (S.fromList [(pApp "Animal" [var "y"]),(pApp "AnimalLover" [var "x"]),(pApp "Kills" [var "x",var "y"])]) (S.fromList []), wiIdent = 3},+                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])]), wiIdent = 4},+                      WithId {wiItem = INF (S.fromList []) (S.fromList [(pApp "Cat" [fApp "Tuna" []])]), wiIdent = 5},+                      WithId {wiItem = INF (S.fromList [(pApp "Cat" [var "x"])]) (S.fromList [(pApp "Animal" [var "x"])]), wiIdent = 6}])+          , ChiouResult (False,+                         (S.fromList+                          [(inf' [(pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])] [],fromList []),+                           (inf' [] [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []])],fromList []),+                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),+                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []]),(pApp "Cat" [fApp "Tuna" []])] [],fromList []),+                           (inf' [(pApp "Animal" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList []),+                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+                           (inf' [(pApp "AnimalLover" [fApp "Curiosity" []])] [],fromList []),+                           (inf' [(pApp "Cat" [fApp "Tuna" []]),(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList []),+                           (inf' [(pApp "Dog" [var "y"]),(pApp "Owns" [fApp "Curiosity" [],var "y"])] [],fromList []),+                           (inf' [(pApp "Owns" [fApp "Curiosity" [],fApp (toSkolem 1) []])] [],fromList [])]))+          ]+      }+    , TestProof+      { proofName = "prove curiosity kills tuna"+      , proofKnowledge = kbKnowledge (animalKB :: (String, [TestFormula formula term v p f]))+      , conjecture = kills [curiosity, tuna]+      , proofExpected =+          [ ChiouKB (S.fromList+                     [WithId {wiItem = inf' []                                 [(pApp "Dog" [fApp (toSkolem 1) []])],                 wiIdent = 1},+                      WithId {wiItem = inf' []                                 [(pApp "Owns" [fApp "Jack" [],fApp (toSkolem 1) []])], wiIdent = 1},+                      WithId {wiItem = inf' [(pApp "Dog" [var "y"]),+                                             (pApp "Owns" [var "x",var "y"])]  [(pApp "AnimalLover" [var "x"])],                      wiIdent = 2},+                      WithId {wiItem = inf' [(pApp "Animal" [var "y"]),+                                             (pApp "AnimalLover" [var "x"]),+                                             (pApp "Kills" [var "x",var "y"])] [], wiIdent = 3},+                      WithId {wiItem = inf' []                                 [(pApp "Kills" [fApp "Curiosity" [],fApp "Tuna" []]),+                                                                                (pApp "Kills" [fApp "Jack" [],fApp "Tuna" []])],      wiIdent = 4},+                      WithId {wiItem = inf' []                                 [(pApp "Cat" [fApp "Tuna" []])],                       wiIdent = 5},+                      WithId {wiItem = inf' [(pApp "Cat" [var "x"])]           [(pApp "Animal" [var "x"])],                           wiIdent = 6}])+          , ChiouResult (True,+                         S.fromList +                         [(makeINF' ([]) ([]),fromList []),+                          (makeINF' ([]) ([(pApp ("Kills") [fApp ("Jack") [],fApp ("Tuna") []])]),fromList []),+                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem 1) []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Animal") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("AnimalLover") [fApp ("Jack") []]),(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Dog") [fApp (toSkolem 1) []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Cat") [fApp ("Tuna") []]),(pApp ("Owns") [fApp ("Jack") [],fApp (toSkolem 1) []])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Dog") [var ("y")]),(pApp ("Owns") [fApp ("Jack") [],var ("y")])]) ([]),fromList []),+                          (makeINF' ([(pApp ("Kills") [fApp ("Curiosity") [],fApp ("Tuna") []])]) ([]),fromList [])])+          ]+      }+{-+  -- Seems not to terminate+    , let (x, u, v, w, e) = (var "x", var "u", var "v", var "w", var "e") in+      TestProof+      { proofName = "chang example 4.3"+      , proofKnowledge = (fst chang43KB, map (convertFOF id id id . formula) (snd chang43KB))+      , conjecture = for_all' ["x"] (pApp "P" [x, x, e] .=>. (for_all' ["u", "v", "w"] (pApp "P" [u, v, w] .=>. pApp "P" [v, u, w])))+      , proofExpected =+          [ChiouResult (True, [])]+      }+-}+    , let x = var "x" in+      TestProof+      { proofName = "socrates is mortal"+      , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+      , conjecture = for_all "x" (socrates [x] .=>. mortal [x])+      , proofExpected = +         [ ChiouKB (S.fromList+                    [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+                     WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+         , ChiouResult (True,+                        S.fromList +                        [(makeINF' ([]) ([]),fromList []),+                         (makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem 3) []])]),fromList []),+                         (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem 3) []])]),fromList []),+                         (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem 3) []])]),fromList []),+                         (makeINF' ([(pApp ("Mortal") [fApp (toSkolem 3) []])]) ([]),fromList [])])]+      }+    , let x = var "x" in+      TestProof+      { proofName = "socrates is not mortal"+      , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+      , conjecture = (.~.) (for_all "x" (socrates [x] .=>. mortal [x]))+      , proofExpected = +         [ ChiouKB (S.fromList+                    [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+                     WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+         , ChiouResult (False+                       ,(S.fromList [(inf' [(pApp "Socrates" [var "x"])] [(pApp "Mortal" [var "x"])],fromList [("x",var "x")])]))]+      }+    , let x = var "x" in+      TestProof+      { proofName = "socrates exists and is not mortal"+      , proofKnowledge = kbKnowledge (socratesKB :: (String, [TestFormula formula term v p f]))+      , conjecture = (.~.) (exists "x" (socrates [x]) .&. for_all "x" (socrates [x] .=>. mortal [x]))+      , proofExpected = +         [ ChiouKB (S.fromList+                    [WithId {wiItem = inf' [(pApp "Human" [var "x"])] [(pApp "Mortal" [var "x"])], wiIdent = 1},+                     WithId {wiItem = inf' [(pApp "Socrates" [var "x"])] [(pApp "Human" [var "x"])], wiIdent = 2}])+         , ChiouResult (False,+                        S.fromList [(makeINF' ([]) ([(pApp ("Human") [fApp (toSkolem 3) []])]),fromList []),+                                    (makeINF' ([]) ([(pApp ("Mortal") [fApp (toSkolem 3) []])]),fromList []),+                                    (makeINF' ([]) ([(pApp ("Socrates") [fApp (toSkolem 3) []])]),fromList []),+                                    (makeINF' ([(pApp ("Socrates") [var ("x")])]) ([(pApp ("Mortal") [var ("x")])]),fromList [("x",var ("x"))])])+         ]+      }+    ]++inf' = makeINF'++toLL = map S.toList . S.toList+toSS = S.fromList . map S.fromList
+ Test/Logic.hs view
@@ -0,0 +1,436 @@+{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,+             ScopedTypeVariables, TypeSynonymInstances, UndecidableInstances #-}+{-# OPTIONS -Wall -Wwarn -fno-warn-name-shadowing -fno-warn-orphans #-}+module Test.Logic (tests) where++import Data.Logic.Classes.Arity (Arity(arity))+import Data.Logic.Classes.Boolean (Boolean(..))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), showFirstOrder, freeVars, substitute)+import Data.Logic.Classes.Literal (Literal)+import Data.Logic.Classes.Logic (Logic(..))+import Data.Logic.Classes.Negatable (Negatable(..))+import Data.Logic.Classes.Skolem (Skolem(..))+import Data.Logic.Classes.Term (Term(..))+import Data.Logic.Classes.Variable (Variable)+import Data.Logic.Classes.Pred (Pred(..), pApp)+import Data.Logic.Normal.Clause (clauseNormalForm)+import Data.Logic.Normal.Skolem (runNormal)+import Data.Logic.Satisfiable (theorem, inconsistant)+import Data.Logic.Test (V(..), AtomicFunction(..), Pr, TFormula, TTerm)+import qualified Data.Set as Set+import Data.String (IsString(fromString))+import PropLogic (PropForm(..), TruthTable, truthTable)+import qualified TextDisplay as TD+import Test.HUnit++-- |Don't use this at home!  It breaks type safety, fromString "True"+-- fromBool True.+instance Boolean String where+    fromBool = show++tests :: Test+tests = TestLabel "Logic" $ TestList (precTests ++ theoremTests)++formCase :: FirstOrderFormula TFormula TTerm V Pr AtomicFunction =>+            String -> TFormula -> TFormula -> Test+formCase s expected input = TestLabel s $ TestCase (assertEqual s expected input)++precTests :: [Test]+precTests =+    [ formCase "Logic - prec test 1"+               (a .&. (b .|. c))+               (a .&. b .|. c)+      -- You can't apply .~. without parens:+      -- :type (.~. a)   -> (FormulaPF -> t) -> t+      -- :type ((.~.) a) -> FormulaPF+    , formCase "Logic - prec test 2"+               (((.~.) a) .&. b)+               ((.~.) a .&. b)+    -- I switched the precedence of .&. and .|. from infixl to infixr to get+    -- some of the test cases to match the answers given on the miami.edu site,+    -- but maybe I should switch them back and adjust the answer given in the+    -- test case.+    , formCase "Logic - prec test 3"+               ((a .&. b) .&. c) -- infixl, with infixr we get (a .&. (b .&. c))+               (a .&. b .&. c)+    , TestCase (assertEqual "Logic - Find a free variable"+                (freeVars (for_all "x" (x .=. y) :: TFormula))+                (Set.singleton "y"))+    , TestCase (assertEqual "Logic - Substitute a variable"+                (map sub+                         [ for_all "x" (x .=. y) {- :: Formula String String -}+                         , for_all "y" (x .=. y) {- :: Formula String String -} ])+                [ for_all "x" (x .=. z) :: TFormula+                , for_all "y" (z .=. y) :: TFormula ])+    ]+    where+      sub f = substitute (head . Set.toList . freeVars $ f) (var "z") f+      a = pApp ("a") []+      b = pApp ("b") []+      c = pApp ("c") []++x :: TTerm+x = var (fromString "x")+y :: TTerm+y = var (fromString "y")+z :: TTerm+z = var (fromString "z")++-- |Here is an example of automatic conversion from a FirstOrderFormula+-- instance to a PropositionalFormula instance.  The result is PropForm+-- a where a is the original type, but the a values will always be+-- "atomic" formulas, never the operators which can be converted into+-- the corresponding operator of a PropositionalFormula instance.+{-+test9a :: Test+test9a = TestCase +           (assertEqual "Logic - convert to PropLogic"+            expected+            (flatten (cnf' (for_all "x" (for_all "y" (q [x, y] .<=>. for_all "z" (f [z, x] .<=>. f [z, y])))))))+    where+      f = pApp "f"+      q = pApp "q"+      expected :: PropForm TFormula+      expected = CJ [DJ [N (A (pApp ("q") [var (V "x"),var (V "y")])),+                         N (A (pApp ("f") [var (V "z"),var (V "x")])),+                         A (pApp ("f") [var (V "z"),var (V "y")])],+                     DJ [N (A (pApp ("q") [var (V "x"),var (V "y")])),+                         N (A (pApp ("f") [var (V "z"),var (V "y")])),+                         A (pApp ("f") [var (V "z"),var (V "x")])],+                     DJ [A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")]),+                         A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")]),+                         A (pApp ("q") [var (V "x"),var (V "y")])],+                     DJ [N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")])),+                         A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")]),+                         A (pApp ("q") [var (V "x"),var (V "y")])],+                     DJ [A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")]),+                         N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")])),+                         A (pApp ("q") [var (V "x"),var (V "y")])],+                     DJ [N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "y")])),+                         N (A (pApp ("f") [fApp (Skolem 1) [var (V "x"),var (V "y"),var (V "z")],var (V "x")])),+                         A (pApp ("q") [var (V "x"),var (V "y")])]]++moveQuantifiersOut1 :: Test+moveQuantifiersOut1 =+    formCase "Logic - moveQuantifiersOut1"+             (for_all "x2" ((pApp ("p") [var ("x2")]) .&. ((pApp ("q") [var ("x")]))))+             (prenexNormalForm (for_all "x" (pApp (fromString "p") [x]) .&. (pApp (fromString "q") [x])))++skolemize1 :: Test+skolemize1 =+    formCase "Logic - skolemize1" expected formula+    where+      expected :: TFormula+      expected = for_all [V "y",V "z"] (for_all [V "v"] (pApp "P" [fApp (toSkolem 1) [], y, z, fApp ((toSkolem 2)) [y, z], v, fApp (toSkolem 3) [y, z, v]]))+      formula :: TFormula+      formula = (snf' (exists ["x"] (for_all ["y", "z"] (exists ["u"] (for_all ["v"] (exists ["w"] (pApp "P" [x, y, z, u, v, w])))))))++skolemize2 :: Test+skolemize2 =+    formCase "Logic - skolemize2" expected formula+    where+      expected :: TFormula+      expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [],y])+      formula :: TFormula+      formula = snf' (exists ["x"] (for_all ["y"] (pApp "loves" [x, y])))++skolemize3 :: Test+skolemize3 =+    formCase "Logic - skolemize3" expected formula+    where+      expected :: TFormula+      expected = for_all [V "y"] (pApp ("loves") [fApp (toSkolem 1) [y],y])+      formula :: TFormula+      formula = snf' (for_all ["y"] (exists ["x"] (pApp "loves" [x, y])))+-}+{-+inf1 :: Test+inf1 =+    formCase "Logic - inf1" expected formula+    where+      expected :: TFormula+      expected = ((pApp ("p") [var ("x")]) .=>. (((pApp ("q") [var ("x")]) .|. ((pApp ("r") [var ("x")])))))+      formula :: {- ImplicativeNormalFormula inf (C.Sentence V String AtomicFunction) (C.Term V AtomicFunction) V String AtomicFunction => -} TFormula+      formula = convertFOF id id id (implicativeNormalForm (convertFOF id id id (for_all ["x"] (p [x] .=>. (q [x] .|. r [x]))) :: C.Sentence V String AtomicFunction) :: C.Sentence V String AtomicFunction)+-}++instance Arity String where+    arity _ = Nothing++theoremTests :: [Test]+theoremTests =+    let s = pApp "S"+        h = pApp "H"+        m = pApp "M" in+    [ let formula = for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>.+                                  (s [x] .=>. m [x])) in+      TestCase (assertEqual "Logic - theorem test 1"+                (True,([],Just (CJ []),[([],True)]))+{-+                (True,+                 ([(pApp ("H") [var (V "x")]),(pApp ("M") [var (V "x")]),(pApp ("S") [var (V "x")])],+                  Just (CJ [DJ [A (pApp ("S") [var (V "x")]),+                                A (pApp ("H") [var (V "x")]),+                                N (A (pApp ("S") [var (V "x")])),+                                A (pApp ("M") [var (V "x")])],+                            DJ [N (A (pApp ("H") [var (V "x")])),+                                A (pApp ("H") [var (V "x")]),+                                N (A (pApp ("S") [var (V "x")])),+                                A (pApp ("M") [var (V "x")])],+                            DJ [A (pApp ("S") [var (V "x")]),+                                N (A (pApp ("M") [var (V "x")])),+                                N (A (pApp ("S") [var (V "x")])),+                                A (pApp ("M") [var (V "x")])],+                            DJ [N (A (pApp ("H") [var (V "x")])),+                                N (A (pApp ("M") [var (V "x")])),+                                N (A (pApp ("S") [var (V "x")])),+                                A (pApp ("M") [var (V "x")])]]),+                  [([False,False,False],True),+                   ([False,False,True],True),+                   ([False,True,False],True),+                   ([False,True,True],True),+                   ([True,False,False],True),+                   ([True,False,True],True),+                   ([True,True,False],True),+                   ([True,True,True],True)]))+-}+                (runNormal (theorem formula), table formula))+    , TestCase (assertEqual "Logic - theorem test 1a"+                (False,+                 False,+                 ([(pApp1 ("H") (fApp (toSkolem 1) [])),+                   (pApp1 ("M") (var ("y"))),+                   (pApp1 ("M") (fApp (toSkolem 1) [])),+                   (pApp1 ("S") (var ("y"))),+                   (pApp1 ("S") (fApp (toSkolem 1) []))],+                  Just (CJ [DJ [A (pApp1 ("H") (fApp (toSkolem 1) [])),+                                A (pApp1 ("M") (var ("y"))),+                                A (pApp1 ("S") (fApp (toSkolem 1) [])),+                                N (A (pApp1 ("S") (var ("y"))))],+                            DJ [A (pApp1 ("M") (var ("y"))),+                                A (pApp1 ("S") (fApp (toSkolem 1) [])),+                                N (A (pApp1 ("M") (fApp (toSkolem 1) []))),+                                N (A (pApp1 ("S") (var ("y"))))],+                            DJ [A (pApp1 ("M") (var ("y"))),+                                N (A (pApp1 ("H") (fApp (toSkolem 1) []))),+                                N (A (pApp1 ("M") (fApp (toSkolem 1) []))),+                                N (A (pApp1 ("S") (var ("y"))))]]),+                  [([False,False,False,False,False],True),+                   ([False,False,False,False,True],True),+                   ([False,False,False,True,False],False),+                   ([False,False,False,True,True],True),+                   ([False,False,True,False,False],True),+                   ([False,False,True,False,True],True),+                   ([False,False,True,True,False],False),+                   ([False,False,True,True,True],True),+                   ([False,True,False,False,False],True),+                   ([False,True,False,False,True],True),+                   ([False,True,False,True,False],True),+                   ([False,True,False,True,True],True),+                   ([False,True,True,False,False],True),+                   ([False,True,True,False,True],True),+                   ([False,True,True,True,False],True),+                   ([False,True,True,True,True],True),+                   ([True,False,False,False,False],True),+                   ([True,False,False,False,True],True),+                   ([True,False,False,True,False],True),+                   ([True,False,False,True,True],True),+                   ([True,False,True,False,False],True),+                   ([True,False,True,False,True],True),+                   ([True,False,True,True,False],False),+                   ([True,False,True,True,True],False),+                   ([True,True,False,False,False],True),+                   ([True,True,False,False,True],True),+                   ([True,True,False,True,False],True),+                   ([True,True,False,True,True],True),+                   ([True,True,True,False,False],True),+                   ([True,True,True,False,True],True),+                   ([True,True,True,True,False],True),+                   ([True,True,True,True,True],True)]))+                +                (let formula = (for_all "x" ((s [x] .=>. h [x]) .&. (h [x] .=>. m [x]))) .=>.+                               (for_all "y" (s [y] .=>. m [y])) in+                 (runNormal (theorem formula), runNormal (inconsistant formula), table formula)))+                +    , TestCase (assertEqual "Logic - socrates is mortal, truth table"+                ([(pApp1 ("H") (var ("x"))),+                  (pApp1 ("M") (var ("x"))),+                  (pApp1 ("S") (var ("x")))],+                 Just (CJ [DJ [A (pApp1 ("H") (var ("x"))),N (A (pApp1 ("S") (var ("x"))))],+                           DJ [A (pApp1 ("M") (var ("x"))),N (A (pApp1 ("H") (var ("x"))))],+                           DJ [A (pApp1 ("M") (var ("x"))),N (A (pApp1 ("S") (var ("x"))))]]),+                 [([False,False,False],True),+                  ([False,False,True],False),+                  ([False,True,False],True),+                  ([False,True,True],False),+                  ([True,False,False],False),+                  ([True,False,True],False),+                  ([True,True,False],True),+                  ([True,True,True],True)])+                -- This formula has separate variables for each of the+                -- three beliefs.  To combine these into an argument+                -- we would wrap a single exists around them all and+                -- remove the existing ones, substituting that one+                -- variable into each formula.+                (table (for_all "x" (s [x] .=>. h [x]) .&.+                         for_all "y" (h [y] .=>. m [y]) .&.+                         for_all "z" (s [z] .=>. m [z]))))++    , TestCase (assertEqual "Logic - socrates is not mortal"+                (False,+                 False,+                 ([(pApp ("H") [var ("x")]),+                   (pApp ("M") [var ("x")]),+                   (pApp ("S") [var ("x")]),+                   (pApp ("S") [fApp ("socrates") []])],+                  Just (CJ [DJ [A (pApp ("H") [var ("x")]),N (A (pApp ("S") [var ("x")]))],+                            DJ [A (pApp ("M") [var ("x")]),N (A (pApp ("H") [var ("x")]))],+                            DJ [A (pApp ("S") [fApp ("socrates") []])],+                            DJ [N (A (pApp ("M") [var ("x")])),N (A (pApp ("S") [var ("x")]))]]),+                  [([False,False,False,False],False),+                   ([False,False,False,True],True),+                   ([False,False,True,False],False),+                   ([False,False,True,True],False),+                   ([False,True,False,False],False),+                   ([False,True,False,True],True),+                   ([False,True,True,False],False),+                   ([False,True,True,True],False),+                   ([True,False,False,False],False),+                   ([True,False,False,True],False),+                   ([True,False,True,False],False),+                   ([True,False,True,True],False),+                   ([True,True,False,False],False),+                   ([True,True,False,True],True),+                   ([True,True,True,False],False),+                   ([True,True,True,True],False)]),+                 toSS [[(pApp ("H") [var ("x")]),((.~.) (pApp ("S") [var ("x")]))],+                       [(pApp ("M") [var ("x")]),((.~.) (pApp ("H") [var ("x")]))],+                       [(pApp ("S") [fApp ("socrates") []])],+                       [((.~.) (pApp ("M") [var ("x")])),((.~.) (pApp ("S") [var ("x")]))]])+                -- This represents a list of beliefs like those in our+                -- database: socrates is a man, all men are mortal,+                -- each with its own quantified variable.  In+                -- addition, we have an inconsistant belief, socrates+                -- is not mortal.  If we had a single variable this+                -- would be inconsistant, but as it stands it is an+                -- invalid argument, there are both 0 and 1 lines in+                -- the truth table.  If we go through the table and+                -- eliminate the lines where S(SkZ(x,y)) is true but M(SkZ(x,y)) is+                -- false (for any x) and those where H(x) is true but+                -- M(x) is false, the remaining lines would all be zero,+                -- the argument would be inconsistant (an anti-theorem.)+                -- How can we modify the formula to make these lines 0?+                (let (formula :: TFormula) =+                         for_all "x" ((s [x] .=>. h [x]) .&.+                                      (h [x] .=>. m [x]) .&.+                                      (m [x] .=>. ((.~.) (s [x])))) .&.+                         (s [fApp "socrates" []]) in+                 (runNormal (theorem formula), runNormal (inconsistant formula), table formula, runNormal (clauseNormalForm formula) :: Set.Set (Set.Set TFormula))))+    , let (formula :: TFormula) =+              (for_all "x" (pApp "L" [var "x"] .=>. pApp "F" [var "x"]) .&. -- All logicians are funny+               exists "x" (pApp "L" [var "x"])) .=>.                            -- Someone is a logician+              (.~.) (exists "x" (pApp "F" [var "x"]))                           -- Someone / Nobody is funny+          input = table formula+          expected = ([(pApp ("F") [var ("x2")]),+                       (pApp ("F") [fApp (toSkolem 1) []]),+                       (pApp ("L") [var ("x")]),+                       (pApp ("L") [fApp (toSkolem 1) []])],+                      Just (CJ [DJ [A (pApp1 ("L") (fApp (toSkolem 1) [])),N (A (pApp1 ("F") (var ("x2")))),N (A (pApp1 ("L") (var ("x"))))],+                                DJ [N (A (pApp1 ("F") (var ("x2")))),N (A (pApp1 ("F") (fApp (toSkolem 1) []))),N (A (pApp1 ("L") (var ("x"))))]]),+                      [([False,False,False,False],True),+                       ([False,False,False,True],True),+                       ([False,False,True,False],True),+                       ([False,False,True,True],True),+                       ([False,True,False,False],True),+                       ([False,True,False,True],True),+                       ([False,True,True,False],True),+                       ([False,True,True,True],True),+                       ([True,False,False,False],True),+                       ([True,False,False,True],True),+                       ([True,False,True,False],False),+                       ([True,False,True,True],True),+                       ([True,True,False,False],True),+                       ([True,True,False,True],True),+                       ([True,True,True,False],False),+                       ([True,True,True,True],False)])+      in TestCase (assertEqual "Logic - gensler189" expected input)+    , let (formula :: TFormula) =+              (for_all "x" (pApp "L" [var "x"] .=>. pApp "F" [var "x"]) .&. -- All logicians are funny+               exists "y" (pApp "L" [var (fromString "y")])) .=>.           -- Someone is a logician+              (.~.) (exists "z" (pApp "F" [var "z"]))                       -- Someone / Nobody is funny+          input = table formula+          expected :: TruthTable TFormula+          expected = ([(pApp1 ("F") (var ("z"))),(pApp1 ("F") (fApp (toSkolem 1) [])),(pApp1 ("L") (var ("y"))),(pApp1 ("L") (fApp (toSkolem 1) []))],Just (CJ [DJ [A (pApp1 ("L") (fApp (toSkolem 1) [])),N (A (pApp1 ("F") (var ("z")))),N (A (pApp1 ("L") (var ("y"))))],DJ [N (A (pApp1 ("F") (var ("z")))),N (A (pApp1 ("F") (fApp (toSkolem 1) []))),N (A (pApp1 ("L") (var ("y"))))]]),[([False,False,False,False],True),([False,False,False,True],True),([False,False,True,False],True),([False,False,True,True],True),([False,True,False,False],True),([False,True,False,True],True),([False,True,True,False],True),([False,True,True,True],True),([True,False,False,False],True),([True,False,False,True],True),([True,False,True,False],False),([True,False,True,True],True),([True,True,False,False],True),([True,True,False,True],True),([True,True,True,False],False),([True,True,True,True],False)])+      in TestCase (assertEqual "Logic - gensler189 renamed" expected input)+    ]++toSS :: Ord a => [[a]] -> Set.Set (Set.Set a)+toSS = Set.fromList . map Set.fromList++{-+theorem5 =+    TestCase (assertEqual "Logic - theorm test 2"+              (Just True)+              (theorem ((.~.) ((for_all "x" (((s [x] .=>. h [x]) .&.+                                               (h [x] .=>. m [x]))) .&.+                                exists "x" (s [x] .&.+                                             ((.~.) (m [x]))))))))+-}++instance TD.Display TFormula where+    textFrame x = [showFirstOrder x]+{-+    textFrame x = [quickShow x]+        where+          quickShow =+              foldF (\ _ -> error "Expecting atoms")+                    (\ _ _ _ -> error "Expecting atoms")+                    (\ _ _ _ -> error "Expecting atoms")+                    (\ t1 op t2 -> quickShowTerm t1 ++ quickShowOp op ++ quickShowTerm t2)+                    (\ p ts -> quickShowPred p ++ "(" ++ intercalate "," (map quickShowTerm ts) ++ ")")+          quickShowTerm =+              foldT quickShowVar+                    (\ f ts -> quickShowFn f ++ "(" ++ intercalate "," (map quickShowTerm ts) ++ ")")+          quickShowVar v = show v+          quickShowPred s = s+          quickShowFn (AtomicFunction s) = s+          quickShowOp (:=:) = "="+          quickShowOp (:!=:) = "!="+-}++{-+-- Truth table tests, find a more reasonable result value than [String].++(theorem1a, theorem1b, theorem1c, theorem1d) =+    ( TestCase (assertEqual "Logic - truth table 1"+                (Just ["foo"])+                (prepare (for_all "x" (((s [x] .=>. h [x]) .&. (h [x] .=>. m [x])) .=>. (s [x] .=>. m [x]))) >>=+                 return . TD.textFrame . truthTable)) )+    where s = pApp "S"+          h = pApp "H"+          m = pApp "M"++type FormulaPF = Formula String String+type F = PropForm FormulaPF++prepare :: FormulaPF -> F+prepare formula = ({- flatten . -} fromJust . toPropositional convertA . cnf . (.~.) $ formula)++convertA = Just . A+-}++table :: forall formula term v p f. (FirstOrderFormula formula term v p f, Literal formula term v p f,+                                     Ord formula, Skolem f, IsString v, Variable v, TD.Display formula) =>+         formula -> TruthTable formula+table f =+    -- truthTable :: Ord a => PropForm a -> TruthTable a+    tt cnf'+    where+      tt :: PropForm formula -> TruthTable formula+      tt = truthTable+      cnf' :: PropForm formula+      cnf' = CJ (map (DJ . map n) cnf)+      cnf :: [[formula]]+      cnf = fromSS (runNormal (clauseNormalForm f))+      fromSS = map Set.toList . Set.toList+      n f = (if negated f then N . A . (.~.) else A) $ f
+ Test/TPTP.hs view
@@ -0,0 +1,22 @@+module Test.TPTP where+    +import Codec.TPTP (Formula)+import Data.Logic.FirstOrder (conj)+import Data.Logic.Instances.TPTP+import Data.Logic.Monad (runNormal)+import Data.Logic.Logic (Logic ((.~.), (.=>.)))+import Data.Logic.Normal (cnfTrace)+import Data.Logic.Test (TestFormula(formula))+import Test.Data (chang43KB, chang43Conjecture)+import Test.HUnit++tests :: Test+tests = TestLabel "TPTP" $ TestList [tptp]++tptp :: Test+tptp =+    TestCase (assertEqual "tptp cnf trace" "abc" (runNormal (cnfTrace f)))+    where+      f :: Formula+      f = (.~.) (conj (map formula (snd (chang43KB :: (String, [TestFormula Formula])))) .=>.+                 formula chang43Conjecture)
+ Test/Test.hs view
@@ -0,0 +1,22 @@+import Data.Logic.Classes.FirstOrder (showFirstOrder)+import Data.Logic.Test (TestFormula, TestProof, V, Pr, AtomicFunction, TFormula, TTerm)+import Data.Logic.Types.FirstOrder+import System.Exit+import Test.HUnit+import qualified Test.Logic as Logic+import qualified Test.Chiou0 as Chiou0+--import qualified Test.TPTP as TPTP+import qualified Test.Data as Data++main :: IO ()+main =+    runTestTT (TestList [Logic.tests,+                         Chiou0.tests,+                         -- TPTP.tests,  -- This has a problem in the rendering code - it loops+                         Data.tests formulas proofs]) >>=+    doCounts+    where+      doCounts counts' = exitWith (if errors counts' /= 0 || failures counts' /= 0 then ExitFailure 1 else ExitSuccess)+      -- Generate the test data with a particular instantiation of FirstOrderFormula.+      formulas = (Data.allFormulas :: [TestFormula TFormula TTerm V Pr AtomicFunction])+      proofs = (Data.proofs :: [TestProof TFormula TTerm V])
+ debian/changelog view
@@ -0,0 +1,368 @@+haskell-logic-classes (0.44) unstable; urgency=low++  * Major re-organization of modules.++ -- David Fox <dsf@seereason.com>  Sun, 09 Oct 2011 17:31:36 -0700++haskell-logic (0.43) unstable; urgency=low++  * Move Propositional modules into Data.Logic.Propositional.+  * Add a Native instance for PropositionalFormula.+  * Add a Normal in the Propositional directory+  * Add clauseNormalForm and disjunctiveNormalForm for Propositional+  * Add clauseNormalFormAlt which is an alternate implementation of+    clauseNormalForm, I'm not sure if it gives results that are actually+    different or just look different, but it makes cabal-debian work.       ++ -- David Fox <dsf@seereason.com>  Thu, 29 Sep 2011 05:56:41 -0700++haskell-logic (0.42) unstable; urgency=low++  * Derive the show instance for ImplicativeNormalForm rather than+    making a custom one.++ -- David Fox <dsf@seereason.com>  Fri, 23 Sep 2011 16:43:09 -0700++haskell-logic (0.41) unstable; urgency=low++  * Add field accessors to Proof type.+  * Finish show implementation for Proof++ -- David Fox <dsf@seereason.com>  Mon, 08 Aug 2011 08:32:56 -0700++haskell-logic (0.40) unstable; urgency=low++  * Remove NoProof constructor from Proof type - we only need this in+    the augumented Proof' type in the ontology package.+  * Add prettyProof and prettyINF to Data.Logic.Pretty.++ -- David Fox <dsf@seereason.com>  Sat, 06 Aug 2011 06:28:20 -0700++haskell-logic (0.39) unstable; urgency=low++  * Move Proof type from ontology to logic.++ -- David Fox <dsf@seereason.com>  Thu, 04 Aug 2011 07:13:00 -0700++haskell-logic (0.38) unstable; urgency=low++  * Remove the triple of function parameters for converting formulas to+    literals, these were all invariably id.++ -- David Fox <dsf@seereason.com>  Tue, 02 Aug 2011 07:34:54 -0700++haskell-logic (0.37) unstable; urgency=low++  * Add an Ord instance to ProofResult so we can insert proofs into sets.++ -- David Fox <dsf@seereason.com>  Mon, 01 Aug 2011 09:51:59 -0700++haskell-logic (0.36) unstable; urgency=low++  * Move module Test.Types to Data.Logic.Test and export so that clients+    of this package can use the definitions to create test cases.++ -- David Fox <dsf@seereason.com>  Sun, 24 Jul 2011 10:45:50 -0700++haskell-logic (0.35) unstable; urgency=low++  * Remove the Pretty class.  Pretty printing of a type is application+    specific, so the type class doesn't make sense.  Instead add function+    parameters to prettyForm et. al. to convert the primitive types to+    Doc.++ -- David Fox <dsf@seereason.com>  Fri, 22 Jul 2011 09:01:45 -0700++haskell-logic (0.34) unstable; urgency=low++  * Allow .=. literals in the Native instance.  This required a fix to the+    resolution prover so that it never did substitutions based on an+    equality predicate which had the same lhs and rhs.++ -- David Fox <dsf@seereason.com>  Thu, 21 Jul 2011 22:30:14 -0700++haskell-logic (0.33) unstable; urgency=low++  * Move the modules into the Data heirarchy.++ -- David Fox <dsf@seereason.com>  Sun, 17 Jul 2011 07:29:49 -0700++haskell-logic (0.32) unstable; urgency=low++  * Add a Pred class to describe predicate application+  * Split pretty printing and show into a module.++ -- David Fox <dsf@seereason.com>  Sat, 16 Jul 2011 15:24:43 -0700++haskell-logic (0.31) unstable; urgency=low++  * Create a second instance of FirstOrderFormula in the module+    Logic.Instances.Public, with Eq and Ord instances that use+    the normal form to detect formulas that are equivalent under+    identity transforms.+  * Export the Bijection class which converts between the public+    and internal formula types.++ -- David Fox <dsf@seereason.com>  Wed, 06 Jul 2011 12:46:45 -0700++haskell-logic (0.30) unstable; urgency=low++  * Simplify the parameters of the ImplicativeNormalForm type in the+    native instance, move it to Logic.Normal and eliminate the+    ImplicativeNormalFormula class.+  * Don't require all formula and term types to be instances of Ord,+    we can just specify it in the functions that need it.++ -- David Fox <dsf@seereason.com>  Sat, 02 Jul 2011 09:20:57 -0700++haskell-logic (0.29) unstable; urgency=low++  * Ported to safe-copy++ -- Jeremy Shaw <jeremy@seereason.com>  Fri, 17 Jun 2011 11:18:32 -0500++haskell-logic (0.28) unstable; urgency=low++  * Switch the order of some constructors so that defaultValue of+    Formula gives us a simpler value.++ -- David Fox <dsf@seereason.com>  Sun, 01 May 2011 11:36:12 -0700++haskell-logic (0.27) unstable; urgency=low++  * Moved JSON instances back to seereason.++ -- David Fox <dsf@seereason.com>  Wed, 13 Apr 2011 20:53:42 -0700++haskell-logic (0.26) unstable; urgency=low++  * Add JSON instances.++ -- David Fox <dsf@seereason.com>  Mon, 04 Apr 2011 07:21:25 -0600++haskell-logic (0.25) unstable; urgency=low++  * Disable the (unused) Logic-TPTP instance, it is blocking the+    ghc7 build.++ -- David Fox <dsf@seereason.com>  Sat, 30 Oct 2010 10:35:35 -0700++haskell-logic (0.24) unstable; urgency=low++  * Add a missing paren in the pretty printing and show instances.++ -- David Fox <dsf@seereason.com>  Wed, 20 Oct 2010 21:17:34 -0700++haskell-logic (0.23) unstable; urgency=low++  * Add a "one" method to the Variable class which returns any instance of+    the class, preferably some general purpose variable name like "x".++ -- David Fox <dsf@seereason.com>  Wed, 06 Oct 2010 12:28:38 -0700++haskell-logic (0.22) unstable; urgency=low++  * Instead of making variables instances of Enum and having non-working+    fromEnum and toEnum methods, create a class Var with only a "next"+    method.+  * Add an Arity class and make it a super class of the predicate types.+  * Replace the pApp method with pApp0, pApp1, pApp2 ... pApp7, add a+    pApp function that checks the predicate arity and dispatches to the+    correct method, or throws an error.+  * Add withUnivQuant to look at the list of universally quantified+    variables wrapped around a formula.++ -- David Fox <dsf@seereason.com>  Fri, 03 Sep 2010 12:36:25 -0700++haskell-logic (0.21.2) unstable; urgency=low++  * Fix a bug in fromFirstOrder+  * Add Logic.Set.cartesianProduct, use to implement allpairs+  * Add purednf and implement purecnf in terms of purednf.++ -- David Fox <dsf@seereason.com>  Mon, 30 Aug 2010 15:44:10 -0700++haskell-logic (0.21) unstable; urgency=low++  * Rename the *Logic classes -> *Formula+  * Split a NormalFormula class out of FirstOrderFormula, use it as+    the result of the clauseNormalForm and implicativeNormalForm+    functions.++ -- David Fox <dsf@seereason.com>  Sun, 29 Aug 2010 14:27:34 -0700++haskell-logic (0.20) unstable; urgency=low++  * Reduce the number of arguments to foldF to three, one for quantifiers,+    one for combining formulas, one for predicates.+  * Add a Predicate type for a temporary representation of a predicate and+    its arguments, this is the type now passed to foldF.++ -- David Fox <dsf@seereason.com>  Mon, 23 Aug 2010 22:14:22 -0700++haskell-logic (0.19) unstable; urgency=low++  * Extensive work on polymorphic version of Resolution prover and test cases.+  * Emergency check-in due to dying disk.+  * Implement skolemization and cnf algorithms from Harrison book.++ -- David Fox <dsf@seereason.com>  Tue, 17 Aug 2010 14:55:39 -0700++haskell-logic (0.18) unstable; urgency=low++  * Remove the Predicate and Proposition synonyms for Formula, they+    seem likely to confuse.++ -- David Fox <dsf@seereason.com>  Wed, 28 Jul 2010 09:30:41 -0700++haskell-logic (0.17) unstable; urgency=low++  * Make all the normal form code polymorphic.++ -- David Fox <dsf@seereason.com>  Mon, 26 Jul 2010 08:05:24 -0700++haskell-logic (0.16) unstable; urgency=low++  * Move important super classes from the individual functions to the type+    class FirstOrderLogic: Eq p, Boolean p, Eq f, Skolem f.+  * Implement a default method for .!=.+  * Remove two "quick simplifications" from Logic.NormalForm.distributeDisjuncts+    because they assume Eq formula, which isn't really well defined.  Can these+    make any difference anyway once we reach CNF?+  * Rename convertPred -> convertFOF to match class name change.++ -- David Fox <dsf@seereason.com>  Sat, 10 Jul 2010 22:25:18 -0700++haskell-logic (0.15) unstable; urgency=low++  * Rename PredicateLogic -> FirstOrderLogic+  * Add a Logic.Prover module with a function to load a knowledgebase.++ -- David Fox <dsf@seereason.com>  Thu, 08 Jul 2010 16:00:35 -0700++haskell-logic (0.14) unstable; urgency=low++  * Fix skolem handling.  Use a Skolem class to convert between Ints+    and skolem functions, and a HasSkolem class to obtain numbers for+    skolem functions from a monad.    +  * Integrate Chiou Prover package into this one.  We need to mix+    pieces of the two.++ -- David Fox <dsf@seereason.com>  Thu, 08 Jul 2010 12:47:23 -0700++haskell-logic (0.13) unstable; urgency=low++  * Implement polymorphic version of implicativeNormalForm.++ -- David Fox <dsf@seereason.com>  Tue, 06 Jul 2010 22:39:55 -0700++haskell-logic (0.12) unstable; urgency=low++  * Parameterize the variable type v in the PredicateLogic class and+    the Formula type in the Parameterized instance.+  * Reduce the number of functional dependencies in the PredicateLogic+    class, this allows us to create two instances that use the same+    types for any of v, p, or f.++ -- David Fox <dsf@seereason.com>  Tue, 06 Jul 2010 17:52:37 -0700++haskell-logic (0.11) unstable; urgency=low++  * Modify the Skolem class so it uses a monad to generate new names+    for skolem functions.  This corresponds to the technique used+    by what is now our only working example of a first order logic+    theorem prover, the new Chiou package.++ -- David Fox <dsf@seereason.com>  Mon, 05 Jul 2010 12:46:08 -0700++haskell-logic (0.10) unstable; urgency=low++  * Add an instance for the Charles Chiou first order logic prover.++ -- David Fox <dsf@seereason.com>  Mon, 05 Jul 2010 09:03:04 -0700++haskell-logic (0.9) unstable; urgency=low++  * Add a Logic.Satisfiable module, containing functions theorem, +    inconsistant, and invalid.++ -- David Fox <dsf@seereason.com>  Fri, 02 Jul 2010 11:34:38 -0700++haskell-logic (0.8) unstable; urgency=low++  * Modify skolemize so it leaves the universal quantifiers on its+    result, and add a function removeUniversal to remove them.  We+    envision having a use for those quantifiers some time soon.+  * Use standard names for the various normal forms, move Logic.CNF+    to Logic.NormalForm.++ -- David Fox <dsf@seereason.com>  Wed, 30 Jun 2010 18:28:00 -0700++haskell-logic (0.7) unstable; urgency=low++  * Change the order of substitution function arguments from (new, old)+    to (old, new), to match the notation generally used in textbooks.++ -- David Fox <dsf@seereason.com>  Wed, 30 Jun 2010 08:58:54 -0700++haskell-logic (0.6.1) unstable; urgency=low++  * Fix a bug in substituteTerm and re-implement skolemize.++ -- David Fox <dsf@seereason.com>  Wed, 30 Jun 2010 06:43:50 -0700++haskell-logic (0.6) unstable; urgency=low++  * Split a Logic class out of PropositionalLogic and make it the ancestor+    of PropositionalLogic and PredicateLogic.  This way we can eliminate+    the horrible atom parameter from the PredicateLogic type.+  * Add a Skolem v f class to encapsulate conversion of variables to+    skolem functions.++ -- David Fox <dsf@seereason.com>  Mon, 28 Jun 2010 06:34:43 -0700++haskell-logic (0.5.1) unstable; urgency=low++  * Rename variables in the moveQuantifiersOut operation of cnf to+    avoid collisions later.+  * Add an Enum instance for the V type so we can find fresh variables,+    and new functions for finding the quantified variables and all the+    variables in a formula.++ -- David Fox <dsf@seereason.com>  Sun, 27 Jun 2010 07:00:49 -0700++haskell-logic (0.5) unstable; urgency=low++  * Export distributeDisjuncts++ -- David Fox <dsf@seereason.com>  Fri, 25 Jun 2010 14:13:44 -0700++haskell-logic (0.4) unstable; urgency=low++  * Add documentation+  * Remove the normalize function+  * Remove the AtomicWord type (use the equivalent in Logic-TPTP.)+  * Make some derived methods into functions.++ -- David Fox <dsf@seereason.com>  Fri, 25 Jun 2010 09:32:22 -0700++haskell-logic (0.3) unstable; urgency=low++  * Eliminate the use of the unicode characters for for_all and+    exists, they make the amd64 version of haddock crash.++ -- David Fox <dsf@seereason.com>  Thu, 24 Jun 2010 13:46:42 -0700++haskell-logic (0.2) unstable; urgency=low++  * Add an Ord instance to AtomicFormula to satisfy the requirements+    of the satisfiable function in PropLogic.++ -- David Fox <dsf@seereason.com>  Thu, 24 Jun 2010 10:08:42 -0700++haskell-logic (0.1) unstable; urgency=low++  * Debianization generated by cabal-debian++ -- David Fox <dsf@seereason.com>  Wed, 23 Jun 2010 14:19:18 -0700+
+ debian/compat view
@@ -0,0 +1,1 @@+7
+ debian/control view
@@ -0,0 +1,83 @@+Source: haskell-logic-classes+Priority: optional+Section: misc+Maintainer: David Fox <dsf@seereason.com>+Build-Depends: debhelper (>= 7.0),+               haskell-devscripts (>= 0.6.15+nmu7),+               hscolour,+               cdbs,+               ghc (>= 6.8),+               ghc-prof,+               libghc-hunit-prof,+               libghc-fgl-prof,+               libghc-happstack-data-prof,+               libghc-incremental-sat-solver-prof,+               libghc-proplogic-prof,+               libghc-mtl-prof,+               libghc-safecopy-prof,+               libghc-set-extra-prof,+               libghc-syb-with-class-prof,+               libghc-text-prof+Build-Depends-Indep: ghc-doc,+                     haddock,+                     libghc-hunit-doc,+                     libghc-fgl-doc,+                     libghc-happstack-data-doc,+                     libghc-incremental-sat-solver-doc,+                     haskell-proplogic-doc,+                     libghc-mtl-doc,+                     libghc-safecopy-doc,+                     libghc-set-extra-doc,+                     libghc-syb-with-class-doc,+                     libghc-text-doc+Standards-Version: 3.8.1++Package: libghc-logic-classes-dev+Architecture: any+Section: haskell+Depends: ${haskell:Depends},+         ${misc:Depends}+Conflicts: libghc-logic-dev+Provides: libghc-logic-dev+Replaces: libghc-logic-dev+Description: Library for unifying various treatments of propositional and first order logic+ Library for unifying various treatments of propositional and first order logic+ .+  Author: David Fox <dsf@seereason.com>+  Upstream-Maintainer: SeeReason Partners <partners@seereason.com>+ .+ This package contains the normal library files.++Package: libghc-logic-classes-prof+Architecture: any+Section: haskell+Depends: ${haskell:Depends},+         ${misc:Depends},+         libghc-logic-dev+Conflicts: libghc-logic-prof+Provides: libghc-logic-prof+Replaces: libghc-logic-prof+Description: Library for unifying various treatments of propositional and first order logic+ Library for unifying various treatments of propositional and first order logic+ .+  Author: David Fox <dsf@seereason.com>+  Upstream-Maintainer: SeeReason Partners <partners@seereason.com>+ .+ This package contains the libraries compiled with profiling enabled.++Package: libghc-logic-classes-doc+Architecture: all+Section: doc+Depends: ${haskell:Depends},+         ${misc:Depends},+         ghc-doc+Conflicts: libghc-logic-doc+Provides: libghc-logic-doc+Replaces: libghc-logic-doc+Description: Library for unifying various treatments of propositional and first order logic+ Library for unifying various treatments of first order logic+ .+  Author: David Fox <dsf@seereason.com>+  Upstream-Maintainer: SeeReason Partners <partners@seereason.com>+ .+ This package contains the documentation files.
+ debian/copyright view
@@ -0,0 +1,1 @@+BSD
+ debian/rules view
@@ -0,0 +1,7 @@+#!/usr/bin/make -f+include /usr/share/cdbs/1/rules/debhelper.mk+include /usr/share/cdbs/1/class/hlibrary.mk++# How to install an extra file into the documentation package+#binary-fixup/libghc6-Logic-doc::+#	echo "Some informative text" > debian/libghc6-Logic-doc/usr/share/doc/libghc6-Logic-doc/AnExtraDocFile
+ logic-classes.cabal view
@@ -0,0 +1,51 @@+Name:             logic-classes+Version:          0.44+License:          BSD3+Author:           David Fox <dsf@seereason.com>+Maintainer:       SeeReason Partners <partners@seereason.com>+Synopsis:         Symbolic logic support - a class framework, example instances, polymorphic implementations+Description:      Package to support Propositional and First Order Logic.  It includes classes+                  representing the different types of formulas and terms, some instances of+                  those classes for types used in other logic libraries, and implementations of+                  several logic algorithms, including conversion to normal form and a simple+                  resolution-based theorem prover for any instance of FirstOrderFormula.+Build-Type:       Custom+Category:         Logic, Theorem Provers+Cabal-version:    >= 1.2++Library+ GHC-options: -threaded -Wall -O2+ Exposed-Modules:  Data.Logic+                   Data.Logic.Classes.Arity+                   Data.Logic.Classes.Boolean+                   Data.Logic.Classes.ClauseNormalForm+                   Data.Logic.Classes.FirstOrder+                   Data.Logic.Classes.Literal+                   Data.Logic.Classes.Logic+                   Data.Logic.Classes.Negatable+                   Data.Logic.Classes.Pred+                   Data.Logic.Classes.Propositional+                   Data.Logic.Classes.Skolem+                   Data.Logic.Classes.Term+                   Data.Logic.Classes.Variable+                   Data.Logic.Instances.Chiou+                   Data.Logic.Instances.PropLogic+                   Data.Logic.Instances.SatSolver+                   Data.Logic.KnowledgeBase+                   Data.Logic.Normal.Clause+                   Data.Logic.Normal.Implicative+                   Data.Logic.Normal.Negation+                   Data.Logic.Normal.Prenex+                   Data.Logic.Normal.Skolem+                   Data.Logic.Resolution+                   Data.Logic.Satisfiable+                   Data.Logic.Types.FirstOrder+                   Data.Logic.Types.FirstOrderPublic+                   Data.Logic.Types.Propositional+ Other-Modules:    Data.Logic.Test+ Build-Depends:    base < 5, containers, fgl, happstack-data, incremental-sat-solver,+                   mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb++Executable tests+ Main-Is: Test/Test.hs+ Build-Depends: HUnit