logic-classes 1.4 → 1.4.1
raw patch · 6 files changed
+20/−19 lines, 6 filesdep ~base
Dependency ranges changed: base
Files
- Data/Logic/Classes/Equals.hs +1/−1
- Data/Logic/Harrison/Herbrand.hs +9/−9
- Data/Logic/Normal/Implicative.hs +1/−1
- Data/Logic/Tests/Common.hs +2/−2
- Data/Logic/Tests/Harrison/Common.hs +2/−2
- logic-classes.cabal +5/−4
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 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 "="
Data/Logic/Harrison/Herbrand.hs view
@@ -1,14 +1,16 @@-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-} module Data.Logic.Harrison.Herbrand where import Control.Applicative.Error (Failing(..)) import Data.Logic.Classes.Atom (Atom(substitute, freeVariables))-import Data.Logic.Classes.FirstOrder (FirstOrderFormula)+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.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)+import Data.Logic.Classes.Term (Term, fApp, vt) import Data.Logic.Harrison.DP (dpll) import Data.Logic.Harrison.FOL (generalize) import Data.Logic.Harrison.Lib (distrib', allpairs)@@ -18,6 +20,7 @@ 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. @@ -133,7 +136,8 @@ Term term v f, Atom atom term v, IsString f,- Ord pf) =>+ Ord pf,+ pf ~ fof) => (atom -> Set.Set (f, Int)) -> fof -> Failing Int gilmore fa fm = let sfm = runSkolem (skolemize id ((.~.)(generalize fm))) :: pf in@@ -145,12 +149,8 @@ -- ------------------------------------------------------------------------- -- 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/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 (Negatable lit, Ord lit) => ImplicativeForm lit =+data 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)
logic-classes.cabal view
@@ -1,5 +1,5 @@ Name: logic-classes-Version: 1.4+Version: 1.4.1 Synopsis: Framework for propositional and first order logic, theorem proving Description: Package to support Propositional and First Order Logic. It includes classes representing the different types of formulas and terms, some instances of@@ -12,7 +12,7 @@ Maintainer: SeeReason Partners <partners@seereason.com> Bug-Reports: http://bugzilla.seereason.com/ Category: Logic, Theorem Provers-Cabal-version: >= 1.6+Cabal-version: >= 1.9 Build-Type: Simple Library@@ -69,13 +69,14 @@ 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, incremental-sat-solver,+ Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, 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: HUnit+ Build-Depends: applicative-extras, base, containers, happstack-data, HUnit, incremental-sat-solver, mtl,+ pretty, PropLogic, safecopy, set-extra, syb, template-haskell Other-Modules: Data.Logic.Tests.Chiou0 Data.Logic.Tests.Common Data.Logic.Tests.Data