License | GNU LGPLv3 |
---|---|
Maintainer | paul.bittner@uni-ulm.de |
Safe Haskell | Safe |
Type class for reasoning on Logic
s.
Documentation
Type class to reason on logics. We use this type class to reason on propositional logic and the ternary logic by Sobocinski we use for feature trace recording.
The atomic value representing true in this logic.
The atomic value representing false in this logic.
Negation of a logical formula.
Conjunction of a list of logical formulas.
Disjunction of a list of logical formulas.
limplies :: l -> l -> l Source #
Implication between two logical formulas.
The first argument p
is one the left side of the implication and the second argument q
is on the right (i.e., p => q
).
lequals :: l -> l -> l Source #
Equivalence between two logical formulas.
leval :: (l -> l) -> l -> l Source #
Evaluates a logical formula. Arguments are
- a function assigning variables to values
- a formula to evaluate
This function should return an element of
lvalues
.
Instances
Logic a => Logic (Maybe a) Source # | Any |
Logic (PropositionalFormula a) Source # |
|
Defined in Propositions ltrue :: PropositionalFormula a Source # lfalse :: PropositionalFormula a Source # lvalues :: [PropositionalFormula a] Source # lnot :: PropositionalFormula a -> PropositionalFormula a Source # land :: [PropositionalFormula a] -> PropositionalFormula a Source # lor :: [PropositionalFormula a] -> PropositionalFormula a Source # limplies :: PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a Source # lequals :: PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a Source # leval :: (PropositionalFormula a -> PropositionalFormula a) -> PropositionalFormula a -> PropositionalFormula a Source # |