Safe Haskell	Safe
Language	Haskell2010

Logic

Synopsis

Documentation

type VarProp = String Source #

data FProp Source #

Constructors

T
F
Atom VarProp
Neg FProp
Conj FProp FProp
Disj FProp FProp
Impl FProp FProp
Equi FProp FProp

Instances

Eq FProp Source #
Methods (==) :: FProp -> FProp -> Bool # (/=) :: FProp -> FProp -> Bool #
Ord FProp Source #
Methods compare :: FProp -> FProp -> Ordering # (<) :: FProp -> FProp -> Bool # (<=) :: FProp -> FProp -> Bool # (>) :: FProp -> FProp -> Bool # (>=) :: FProp -> FProp -> Bool # max :: FProp -> FProp -> FProp # min :: FProp -> FProp -> FProp #
Show FProp Source #
Methods showsPrec :: Int -> FProp -> ShowS # show :: FProp -> String # showList :: [FProp] -> ShowS #
Arbitrary FProp Source #
Methods arbitrary :: Gen FProp shrink :: FProp -> [FProp]

p :: FProp Source #

q :: FProp Source #

r :: FProp Source #

no :: FProp -> FProp Source #

(∨) :: FProp -> FProp -> FProp infixr 5 Source #

(∧) :: FProp -> FProp -> FProp infixr 4 Source #

(→) :: FProp -> FProp -> FProp infixr 3 Source #

(<->) :: FProp -> FProp -> FProp infixr 2 Source #

substitute :: FProp -> VarProp -> FProp -> FProp Source #

For example, >>> substitute (no p) "p" q ¬q >>> substitute (no (q ∧ no p)) "p" (q ↔ p) ¬(q ∧ ¬(q ↔ p))

type Interpretation = [FProp] Source #

signify :: FProp -> Interpretation -> Bool Source #

For example,

>>> signify ((p ∨ q) ∧ ((no q) ∨ r)) [r]
False
>>> signify ((p ∨ q) ∧ ((no q) ∨ r)) [p,r]
True

isModelForm :: Interpretation -> FProp -> Bool Source #

For example,

>>> isModelForm [r]   ((p ∨ q) ∧ ((no q) ∨ r))
False
>>> isModelForm [p,r] ((p ∨ q) ∧ ((no q) ∨ r))
True

propSymbolsForm :: FProp -> [FProp] Source #

For example,

>>> propSymbolsForm (p ∧ q → p)
[p,q]

interpretationsForm :: FProp -> [Interpretation] Source #

For example,

>>> interpretationsForm (p ∧ q → p)
[[],[p],[q],[p,q]]

modelsForm :: FProp -> [Interpretation] Source #

For example,

>>> modelsForm ((p ∨ q) ∧ ((no q) ∨ r))
[[p],[p,r],[q,r],[p,q,r]]

isValid :: FProp -> Bool Source #

For example,

>>> isValid (p → p)
True
>>> isValid (p → q)
False
>>> isValid ((p → q) ∨ (q → p))
True

isUnsatisfiable :: FProp -> Bool Source #

For example,

>>> isUnsatisfiable (p ∧ (no p))
True
>>> isUnsatisfiable ((p → q) ∧ (q → r))
False

isSatisfiable :: FProp -> Bool Source #

For example,

>>> isSatisfiable (p ∧ (no p))
False
>>> isSatisfiable ((p → q) ∧ (q → r))
True

type KB = Set FProp Source #

propSymbolsKB :: KB -> [FProp] Source #

For example,

>>> propSymbolsKB (S.fromList [p ∧ q → r, p → r])
[p,r,q]

interpretationsKB :: KB -> [Interpretation] Source #

For example,

>>> interpretationsKB (S.fromList [p → q, q → r])
[[],[p],[q],[p,q],[r],[p,r],[q,r],[p,q,r]]

isModelKB :: Interpretation -> KB -> Bool Source #

For example,

>>> isModelKB [r] (S.fromList [q,no p ,r])
False
>>> isModelKB [q,r] (S.fromList [q,no p ,r])
True

modelsKB :: KB -> [Interpretation] Source #

For example,

>>> modelsKB $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), q → r]
[[p],[p,r],[q,r],[p,q,r]]
>>> modelsKB $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), r → q]
[[p],[q,r],[p,q,r]]

isConsistent :: KB -> Bool Source #

For example,

>>> isConsistent $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), p → r]
True
>>> isConsistent $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), p → r, no r]
False

isInconsistent :: KB -> Bool Source #

For example,

>>> isInconsistent $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), p → r]
False
>>> isInconsistent $ S.fromList [(p ∨ q) ∧ ((no q) ∨ r), p → r, no r]
True

isConsequence :: KB -> FProp -> Bool Source #

For example,

>>> isConsequence (S.fromList [p → q, q → r]) (p → r)
True
>>> isConsequence (S.fromList [p]) (p ∧ q)
False

prop_isValid :: FProp -> Bool Source #

>>> quickCheck prop_isValid
+++ OK, passed 100 tests.

prop_isConsequence :: KB -> FProp -> Bool Source #

>>> quickCheck prop_isConsequence
+++ OK, passed 100 tests.

isConsequenceKB :: KB -> KB -> Bool Source #

For example,

>>> isConsequenceKB (S.fromList [p → q, q → r]) (S.fromList [p → q, p → r])
True
>>> isConsequenceKB (S.fromList [p]) (S.fromList [p ∧ q])
False

equivalent :: FProp -> FProp -> Bool Source #

For example,

>>> equivalent (p → q) (no p ∨ q)
True
>>> equivalent (p) (no (no p))
True

equivalentKB :: KB -> KB -> Bool Source #

For example,

>>> equivalentKB (S.fromList [p → q,r ∨ q]) (S.fromList [no p ∨ q, q ∨ r])
True
>>> equivalentKB (S.fromList [p ∧ q]) (S.fromList [q,p])
True

prop_equivalent :: FProp -> FProp -> Bool Source #

>>> quickCheck prop_equivalent
+++ OK, passed 100 tests.