Data.Logic.Classes.ClauseNormalForm

Documentation

class (Negatable lit, Eq lit, Ord lit) => ClauseNormalFormula cnf lit | cnf -> lit where

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)

makeCNF :: Set (Set lit) -> cnf

satisfiable :: MonadPlus m => cnf -> m Bool

Instances

ClauseNormalFormula CNF Literal