logic-classes 0.45 → 0.47
raw patch · 7 files changed
+62/−38 lines, 7 filesdep ~base
Dependency ranges changed: base
Files
- Data/Logic/KnowledgeBase.hs +39/−22
- Data/Logic/Normal/Implicative.hs +2/−2
- Data/Logic/Normal/Skolem.hs +3/−3
- Data/Logic/Resolution.hs +11/−4
- Data/Logic/Test.hs +3/−3
- Data/Logic/Types/FirstOrderPublic.hs +1/−1
- logic-classes.cabal +3/−3
Data/Logic/KnowledgeBase.hs view
@@ -1,5 +1,5 @@-{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, RankNTypes,- TypeSynonymInstances, UndecidableInstances #-}+{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings, PackageImports,+ RankNTypes, TemplateHaskell, TypeSynonymInstances, UndecidableInstances #-} {-# OPTIONS -Wall #-} {- KnowledgeBase.hs -}@@ -24,9 +24,9 @@ , showKB ) where -import Control.Monad.Identity (Identity(runIdentity))-import Control.Monad.State (StateT, evalStateT, MonadState(get, put))-import Control.Monad.Trans (lift)+import "mtl" Control.Monad.Identity (Identity(runIdentity))+import "mtl" Control.Monad.State (StateT, evalStateT, MonadState(get, put))+import "mtl" Control.Monad.Trans (lift) import Data.Generics (Data, Typeable) import Data.Logic.Classes.FirstOrder (FirstOrderFormula) import Data.Logic.Classes.Negatable (Negatable(..))@@ -34,7 +34,9 @@ import Data.Logic.Normal.Implicative (ImplicativeForm, implicativeNormalForm) import Data.Logic.Normal.Skolem (NormalT, runNormalT) import Data.Logic.Resolution (prove, SetOfSupport, getSetOfSupport)+import Data.SafeCopy (deriveSafeCopy, base) import qualified Data.Set.Extra as S+import Happstack.Data (Default(defaultValue), deriveNewDataNoDefault) import Prelude hiding (negate) type SentenceCount = Int@@ -62,24 +64,27 @@ data ProverState inf = ProverState- { knowledgeBase :: KnowledgeBase inf+ { recursionLimit :: Maybe Int+ , knowledgeBase :: KnowledgeBase inf , sentenceCount :: Int } -zeroKB :: ProverState inf-zeroKB = ProverState- { knowledgeBase = S.empty+zeroKB :: Maybe Int -> ProverState inf+zeroKB limit =+ ProverState+ { recursionLimit = limit+ , 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'+runProverT' :: Monad m => Maybe Int -> ProverT' v term inf m a -> m a+runProverT' limit = runNormalT . runProverT limit+runProverT :: Monad m => Maybe Int -> StateT (ProverState inf) m a -> m a+runProverT limit action = evalStateT action (zeroKB limit)+runProver' :: Maybe Int -> ProverT' v term inf Identity a -> a+runProver' limit = runIdentity . runProverT' limit {- runProver :: StateT (ProverState inf) Identity a -> a runProver = runIdentity . runProverT@@ -94,6 +99,13 @@ -- ^ Both are satisfiable deriving (Data, Typeable, Eq, Ord, Show) +$(deriveSafeCopy 1 'base ''ProofResult)++$(deriveNewDataNoDefault [''ProofResult])++instance Default ProofResult where+ defaultValue = Invalid+ 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@@ -112,26 +124,31 @@ -- |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) =>+inconsistantKB :: forall m formula term v p f lit. (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) => 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+inconsistantKB s =+ get >>= \ st ->+ lift (implicativeNormalForm s) >>=+ return . getSetOfSupport >>= \ sos ->+ getKB >>=+ return . prove (recursionLimit st) 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) =>+theoremKB :: forall m formula term v p f lit. (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f, Show term) => 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) =>+askKB :: (Monad m, FirstOrderFormula formula term v p f, Literal lit term v p f, Show term) => 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) =>+validKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) => formula -> ProverT' v term (ImplicativeForm lit) m (ProofResult, SetOfSupport lit v term, SetOfSupport lit v term) validKB s = theoremKB s >>= \ (proved, proof1) ->@@ -141,7 +158,7 @@ -- |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) =>+tellKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) => formula -> ProverT' v term (ImplicativeForm lit) m (Proof lit) tellKB s = do st <- get@@ -154,7 +171,7 @@ , 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) =>+loadKB :: (FirstOrderFormula formula term v p f, Literal lit term v p f, Monad m, Show term) => [formula] -> ProverT' v term (ImplicativeForm lit) m [Proof lit] loadKB sentences = mapM tellKB sentences
Data/Logic/Normal/Implicative.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DeriveDataTypeable, RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable, PackageImports, RankNTypes, ScopedTypeVariables #-} {-# OPTIONS -Wall #-} module Data.Logic.Normal.Implicative ( ImplicativeForm(INF, neg, pos)@@ -11,7 +11,7 @@ import Data.Logic.Normal.Clause (clauseNormalForm) import Data.Logic.Normal.Skolem (NormalT) -import Control.Monad.State (MonadPlus, msum)+import "mtl" Control.Monad.State (MonadPlus, msum) import Data.Generics (Data, Typeable, listify) import Data.List (intersperse) import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..))
Data/Logic/Normal/Skolem.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE PackageImports, RankNTypes, ScopedTypeVariables #-} {-# OPTIONS -Wall #-} module Data.Logic.Normal.Skolem ( LiteralMapT@@ -14,8 +14,8 @@ 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 "mtl" Control.Monad.Identity (Identity(runIdentity))+import "mtl" 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(..))
Data/Logic/Resolution.hs view
@@ -26,15 +26,22 @@ 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 =+prove :: (Literal lit term v p f, Show v, Show term) =>+ Maybe Int -- ^ Recursion limit. We continue recursing until this+ -- becomes zero. If it is negative it may recurse until+ -- it overflows the stack.+ -> SetOfSupport lit v term+ -> SetOfSupport lit v term+ -> S.Set (ImplicativeForm lit)+ -> (Bool, SetOfSupport lit v term)+prove (Just 0) ss1 _ _ = (False, ss1)+prove limit 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)+ (ss', False) -> prove (maybe Nothing (\ n -> Just (n - 1)) limit) (S.insert s ss1) ss' (S.insert (fst s) kb) -- prove ss1 [] _kb = (False, ss1) -- prove ss1 (s:ss2) kb = -- let
Data/Logic/Test.hs view
@@ -182,7 +182,7 @@ 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)))+ TestCase (assertEqual (name f ++ " Chiou KB") result (runProver' Nothing (loadKB [formula f] >>= return . head))) doExpected (PropLogicSat result) = TestCase (assertEqual (name f ++ " PropLogic.satisfiable") result (runNormal (plSat (formula f)))) doExpected (SatSolverCNF result) =@@ -233,11 +233,11 @@ [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)))]]+ (runProver' Nothing (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)))]]+ (runProver' Nothing (loadKB kb >> getKB)))]] kb = snd (proofKnowledge p) :: [formula] c = conjecture p :: formula
Data/Logic/Types/FirstOrderPublic.hs view
@@ -8,6 +8,7 @@ module Data.Logic.Types.FirstOrderPublic ( Formula(..)+ , Bijection(..) ) where import Data.Data (Data)@@ -15,7 +16,6 @@ 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(..))
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name: logic-classes-Version: 0.45+Version: 0.47 License: BSD3 Author: David Fox <dsf@seereason.com> Maintainer: SeeReason Partners <partners@seereason.com>@@ -14,7 +14,7 @@ Cabal-version: >= 1.2 Library- GHC-options: -threaded -Wall -O2+ GHC-options: -Wall -O2 Exposed-Modules: Data.Logic Data.Logic.Classes.Arity Data.Logic.Classes.Boolean@@ -43,7 +43,7 @@ Data.Logic.Types.FirstOrderPublic Data.Logic.Types.Propositional Other-Modules: Data.Logic.Test- Build-Depends: base < 5, containers, fgl, happstack-data, incremental-sat-solver,+ Build-Depends: base >= 4.3 && < 5, containers, fgl, happstack-data, incremental-sat-solver, mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb Executable tests