logic-classes-1.5.2: Framework for propositional and first order logic, theorem proving

Safe HaskellSafe-Inferred
LanguageHaskell98

Data.Logic.Classes.ClauseNormalForm

Synopsis

Documentation

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

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) -> cnf Source

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