RSolve.PropLogic

Propositional logic infrastructures Author: Taine Zhao(thautwarm) Date: 2019-08-03 License: MIT

Documentation

class (Show a, Ord a) => AtomF a where

Methods

notA :: a -> [a]

Specifies how to handle the negations. For the finite and enumerable solutions, we can return its supplmentary set.

Instances

AtomF Unif

Defined in RSolve.HM

Methods

notA :: Unif -> [Unif]

data WFF a

Constructors

Atom a

Atom formula, should be specified by the problem

Not (WFF a)

(WFF a) :&&: (WFF a) infixl 5

And

(WFF a) :||: (WFF a) infixl 3

Or

(WFF a) :=>: (WFF a) infixl 3

Implication

Instances

Functor WFF

Defined in RSolve.PropLogic

Methods

fmap :: (a -> b) -> WFF a -> WFF b

(<$) :: a -> WFF b -> WFF a

Eq a => Eq (WFF a)

Defined in RSolve.PropLogic

Methods

(==) :: WFF a -> WFF a -> Bool

(/=) :: WFF a -> WFF a -> Bool

Ord a => Ord (WFF a)

Defined in RSolve.PropLogic

Methods

compare :: WFF a -> WFF a -> Ordering

(<) :: WFF a -> WFF a -> Bool

(<=) :: WFF a -> WFF a -> Bool

(>) :: WFF a -> WFF a -> Bool

(>=) :: WFF a -> WFF a -> Bool

max :: WFF a -> WFF a -> WFF a

min :: WFF a -> WFF a -> WFF a

data NF a

normalized WWF, where '[NF a]' the disjunctive normal form.

Constructors

AtomN a

(NF a) :&& (NF a) infixl 5

(NF a) :|| (NF a) infixl 3

Instances

Functor NF

Defined in RSolve.PropLogic

Methods

fmap :: (a -> b) -> NF a -> NF b

(<$) :: a -> NF b -> NF a

Eq a => Eq (NF a)

Defined in RSolve.PropLogic

Methods

(==) :: NF a -> NF a -> Bool

(/=) :: NF a -> NF a -> Bool

Ord a => Ord (NF a)

Defined in RSolve.PropLogic

Methods

compare :: NF a -> NF a -> Ordering

(<) :: NF a -> NF a -> Bool

(<=) :: NF a -> NF a -> Bool

(>) :: NF a -> NF a -> Bool

(>=) :: NF a -> NF a -> Bool

max :: NF a -> NF a -> NF a

min :: NF a -> NF a -> NF a

assertNF :: AtomF a => NF a -> MS (Set a) ()

normal :: AtomF a => WFF a -> NF a

assert :: AtomF a => WFF a -> MS (Set a) ()

Use a propositinal logic formula to build logic equations incrementally.

unionEquations :: AtomF a => MS (Set a) () -> [[a]]

Produced a list of disjunctions of conjunctive clauses.