RSolve-2.0.0.0

RSolve.PropLogic

Description

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

Synopsis

# Documentation

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

Methods

notA :: a -> [a] Source #

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

Instances
 Source # Instance detailsDefined in RSolve.HM MethodsnotA :: Unif -> [Unif] Source #

data WFF a Source #

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
 Source # Instance detailsDefined in RSolve.PropLogic Methodsfmap :: (a -> b) -> WFF a -> WFF b #(<$) :: a -> WFF b -> WFF a # Eq a => Eq (WFF a) Source # Instance detailsDefined in RSolve.PropLogic Methods(==) :: WFF a -> WFF a -> Bool #(/=) :: WFF a -> WFF a -> Bool # Ord a => Ord (WFF a) Source # Instance detailsDefined in RSolve.PropLogic Methodscompare :: 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 Source # 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  Source # Instance detailsDefined in RSolve.PropLogic Methodsfmap :: (a -> b) -> NF a -> NF b #(<$) :: a -> NF b -> NF a # Eq a => Eq (NF a) Source # Instance detailsDefined in RSolve.PropLogic Methods(==) :: NF a -> NF a -> Bool #(/=) :: NF a -> NF a -> Bool # Ord a => Ord (NF a) Source # Instance detailsDefined in RSolve.PropLogic Methodscompare :: 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) () Source #

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

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

Use a propositinal logic formula to build logic equations incrementally.

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

Produced a list of disjunctions of conjunctive clauses.