Safe Haskell | Safe-Inferred |
---|
Data.Logic.Classes.ClauseNormalForm
Documentation
class (Negatable lit, Eq lit, Ord lit) => ClauseNormalFormula cnf lit | cnf -> lit whereSource
A class to represent formulas in CNF, which is the conjunction of a set of disjuncted literals each which may or may not be negated.
Methods
clauses :: cnf -> Set (Set lit)Source
makeCNF :: Set (Set lit) -> cnfSource
satisfiable :: MonadPlus m => cnf -> m BoolSource
Instances