logic-classes 1.4.5 → 1.4.6

raw patch · 4 files changed

+4/−4 lines, 4 files

Files

• Data/Logic/Classes/Equals.hs +1/−1
• Data/Logic/Instances/SatSolver.hs +1/−1
• Data/Logic/Normal/Implicative.hs +1/−1
• logic-classes.cabal +1/−1

@@ -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 Ord p => PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show)+data PredicateName p = Named p Int | Equals deriving (Eq, Ord, Show)  instance (Pretty p, Ord p) => Pretty (PredicateName p) where     pretty Equals = text "="

@@ -4,7 +4,7 @@  import Control.Monad.State (get, put) import Control.Monad.Trans (lift)-import Data.Boolean.SatSolver+import Data.Boolean.SatSolver (Literal(Pos, Neg), CNF, newSatSolver, assertTrue', solve) import Data.Generics (Data, Typeable) import qualified Data.Set.Extra as S import Data.Logic.Classes.Atom (Atom)

@@ -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 (Negatable lit, Ord lit) => ImplicativeForm lit =+data ImplicativeForm lit =     INF {neg :: Set.Set lit, pos :: Set.Set lit}     deriving (Eq, Ord, Data, Typeable, Show) 

@@ -1,5 +1,5 @@ Name:             logic-classes-Version:          1.4.5+Version:          1.4.6 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