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

Safe HaskellNone
LanguageHaskell98

Data.Logic.Classes.Literal

Synopsis

Documentation

class (Negatable lit, Constants lit, HasFixity atom, Formula lit atom, Ord lit) => Literal lit atom | lit -> atom where Source

Literals are the building blocks of the clause and implicative normal |forms. They support negation and must include True and False elements.

Methods

foldLiteral :: (lit -> r) -> (Bool -> r) -> (atom -> r) -> lit -> r Source

Instances

(Pretty atom, HasFixity atom, Ord atom) => Literal (Formula atom) atom 
Formula (Formula FOLEQ) FOLEQ => Literal (Formula FOLEQ) FOLEQ 
(HasFixity atom, Pretty atom, Ord atom) => Literal (Formula atom) atom 
(Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f)) 

zipLiterals :: Literal lit atom => (lit -> lit -> Maybe r) -> (Bool -> Bool -> Maybe r) -> (atom -> atom -> Maybe r) -> lit -> lit -> Maybe r Source

toPropositional :: forall lit atom pf atom2. (Literal lit atom, PropositionalFormula pf atom2) => (atom -> atom2) -> lit -> pf Source

prettyLit :: forall lit atom v. Literal lit atom => (Int -> atom -> Doc) -> (v -> Doc) -> Int -> lit -> Doc Source

foldAtomsLiteral :: Literal lit atom => (r -> atom -> r) -> r -> lit -> r Source