logic-classes 1.4.1 → 1.4.2
raw patch · 12 files changed
+53/−37 lines, 12 filesdep −happstack-data
Dependencies removed: happstack-data
Files
- COPYING +34/−0
- Data/Logic/Classes/Equals.hs +1/−1
- Data/Logic/Classes/FirstOrder.hs +0/−4
- Data/Logic/Classes/Propositional.hs +0/−3
- Data/Logic/Harrison/Herbrand.hs +9/−9
- Data/Logic/KnowledgeBase.hs +0/−6
- Data/Logic/Normal/Implicative.hs +1/−1
- Data/Logic/Tests/Common.hs +2/−2
- Data/Logic/Tests/Harrison/Common.hs +2/−2
- Data/Logic/Types/FirstOrder.hs +0/−3
- Data/Logic/Types/FirstOrderPublic.hs +0/−3
- logic-classes.cabal +4/−3
+ COPYING view
@@ -0,0 +1,34 @@+This package was cabalized by David Fox+<dsf@seereason.com> on June 18, 2010.++Copyright (c) 2010, 2011, 2012, David Fox++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * The names of contributors may not be used to endorse or promote+ products derived from this software without specific prior+ written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
Data/Logic/Classes/Equals.hs view
@@ -49,7 +49,7 @@ -- | A way to represent any predicate's name. Frequently the equality -- predicate has no standalone representation in the p type, it is -- just a constructor in the atom type, or even the formula type.-data PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show)+data Ord p => PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show) instance (Pretty p, Ord p) => Pretty (PredicateName p) where pretty Equals = text "="
Data/Logic/Classes/FirstOrder.hs view
@@ -44,7 +44,6 @@ import Data.Logic.Classes.Variable (Variable) import Data.SafeCopy (base, deriveSafeCopy) import qualified Data.Set as Set-import Happstack.Data (deriveNewData) import Text.PrettyPrint (Doc, (<>), (<+>), text, parens, nest) -- |The 'FirstOrderFormula' type class. Minimal implementation:@@ -302,6 +301,3 @@ atom_union f fm = overatoms (\ h t -> Set.union (f h) t) fm Set.empty $(deriveSafeCopy 1 'base ''Quant)--$(deriveNewData [''Quant])-
Data/Logic/Classes/Propositional.hs view
@@ -35,7 +35,6 @@ import Data.Logic.Classes.Pretty (Pretty, HasFixity(fixity), Fixity(Fixity), FixityDirection(..)) import Data.SafeCopy (base, deriveSafeCopy) import qualified Data.Set.Extra as Set-import Happstack.Data (deriveNewData) import Text.PrettyPrint (Doc, text, (<>)) -- |A type class for propositional logic. If the type we are writing@@ -332,5 +331,3 @@ $(deriveSafeCopy 1 'base ''BinOp) $(deriveSafeCopy 1 'base ''Combination)--$(deriveNewData [''BinOp, ''Combination])
Data/Logic/Harrison/Herbrand.hs view
@@ -1,16 +1,14 @@-{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-} module Data.Logic.Harrison.Herbrand where import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(substitute, freeVariables))-import Data.Logic.Classes.Combine ((.=>.))-import Data.Logic.Classes.Equals (pApp, funcsAtomEq)-import Data.Logic.Classes.FirstOrder (FirstOrderFormula(exists, for_all))+import Data.Logic.Classes.FirstOrder (FirstOrderFormula) import Data.Logic.Classes.Formula (Formula(..)) import Data.Logic.Classes.Literal (Literal) import Data.Logic.Classes.Negate ((.~.)) import Data.Logic.Classes.Propositional (PropositionalFormula)-import Data.Logic.Classes.Term (Term, fApp, vt)+import Data.Logic.Classes.Term (Term, fApp) import Data.Logic.Harrison.DP (dpll) import Data.Logic.Harrison.FOL (generalize) import Data.Logic.Harrison.Lib (distrib', allpairs)@@ -20,7 +18,6 @@ import qualified Data.Map as Map import qualified Data.Set as Set import Data.String (IsString(..))-import Test.HUnit (Test(..), assertEqual) -- ========================================================================= -- Relation between FOL and propositonal logic; Herbrand theorem. @@ -136,8 +133,7 @@ Term term v f, Atom atom term v, IsString f,- Ord pf,- pf ~ fof) =>+ Ord pf) => (atom -> Set.Set (f, Int)) -> fof -> Failing Int gilmore fa fm = let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in@@ -149,8 +145,12 @@ -- ------------------------------------------------------------------------- -- First example and a little tracing. -- ------------------------------------------------------------------------- - {-+test01 =+ let fm = exists "x" (for_all "y" (pApp "p" [vt "x"] .=>. pApp "p" [vt "y"]))+ sfm = skolemize ((.~.) fm) in+ TestList [TestCase (assertEqual "gilmore 1" 2 (gilmore fm))]+ START_INTERACTIVE;; gilmore <<exists x. forall y. P(x) ==> P(y)>>;;
Data/Logic/KnowledgeBase.hs view
@@ -40,7 +40,6 @@ 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@@ -104,11 +103,6 @@ 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)
Data/Logic/Normal/Implicative.hs view
@@ -52,7 +52,7 @@ -- 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 ImplicativeForm lit =+data (Negatable lit, Ord lit) => ImplicativeForm lit = INF {neg :: Set.Set lit, pos :: Set.Set lit} deriving (Eq, Ord, Data, Typeable, Show)
Data/Logic/Tests/Common.hs view
@@ -177,7 +177,7 @@ instance Eq Doc where a == b = show a == show b -data {- (formula ~ TFormula, atom ~ TAtom, v ~ V) => -} TestFormula formula atom v+data (formula ~ TFormula, atom ~ TAtom, v ~ V) => TestFormula formula atom v = TestFormula { formula :: formula , name :: String@@ -185,7 +185,7 @@ } -- deriving (Data, Typeable) -- |Some values that we might expect after transforming the formula.-data {- (FirstOrderFormula formula atom v, formula ~ TFormula, atom ~ TAtom, v ~ V) => -} Expected formula atom v+data (FirstOrderFormula formula atom v, formula ~ TFormula, atom ~ TAtom, v ~ V) => Expected formula atom v = FirstOrderFormula formula | SimplifiedForm formula | NegationNormalForm formula
Data/Logic/Tests/Harrison/Common.hs view
@@ -4,7 +4,7 @@ import Data.Logic.Types.Harrison.Equal (FOLEQ(..)) import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula(..)) --- deriving instance Show FOLEQ--- deriving instance Show (Formula FOLEQ)+deriving instance Show FOLEQ+deriving instance Show (Formula FOLEQ)
Data/Logic/Types/FirstOrder.hs view
@@ -29,7 +29,6 @@ import Data.Logic.Resolution (isRenameOfAtomEq, getSubstAtomEq) import Data.SafeCopy (SafeCopy, base, deriveSafeCopy, extension, MigrateFrom(..)) 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@@ -201,8 +200,6 @@ $(deriveSafeCopy 1 'base ''PTerm) $(deriveSafeCopy 1 'base ''Formula) $(deriveSafeCopy 2 'extension ''Predicate)--$(deriveNewData [''PTerm, ''Formula, ''Predicate]) -- Migration --
Data/Logic/Types/FirstOrderPublic.hs view
@@ -27,7 +27,6 @@ import Data.SafeCopy (base, deriveSafeCopy) import Data.Set (Set) import Data.Typeable (Typeable)-import Happstack.Data (deriveNewData) -- |Convert between the public and internal representations. class Bijection p i where@@ -115,5 +114,3 @@ pretty formula = prettyFirstOrder (\ _prec a -> pretty a) pretty 0 formula $(deriveSafeCopy 1 'base ''Formula)--$(deriveNewData [''Formula])
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name: logic-classes-Version: 1.4.1+Version: 1.4.2 Synopsis: Framework for propositional and first order logic, theorem proving Description: Package to support Propositional and First Order Logic. It includes classes representing the different types of formulas and terms, some instances of@@ -8,6 +8,7 @@ resolution-based theorem prover for any instance of FirstOrderFormula. Homepage: http://src.seereason.com/logic-classes License: BSD3+License-File: COPYING Author: David Fox <dsf@seereason.com> Maintainer: SeeReason Partners <partners@seereason.com> Bug-Reports: http://bugzilla.seereason.com/@@ -69,13 +70,13 @@ Data.Logic.Types.Harrison.Formulas.Propositional Data.Logic.Types.Harrison.Prop Data.Logic.Types.Propositional- Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, HUnit, incremental-sat-solver,+ Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit, incremental-sat-solver, mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb, template-haskell Executable tests GHC-Options: -Wall -O2 Main-Is: Data/Logic/Tests/Main.hs- Build-Depends: applicative-extras, base, containers, happstack-data, HUnit, incremental-sat-solver, mtl,+ Build-Depends: applicative-extras, base, containers, HUnit, incremental-sat-solver, mtl, pretty, PropLogic, safecopy, set-extra, syb, template-haskell Other-Modules: Data.Logic.Tests.Chiou0 Data.Logic.Tests.Common