Safe Haskell | None |
---|

- eval :: FirstOrderFormula formula atom v => formula -> (atom -> Bool) -> Bool
- list_disj :: (Constants formula, Combinable formula) => Set formula -> formula
- list_conj :: (Constants formula, Combinable formula) => Set formula -> formula
- var :: forall formula atom term v. (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set v
- fv :: forall formula atom term v. (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set v
- subst :: (FirstOrderFormula formula atom v, Term term v f, Atom atom term v) => Map v term -> formula -> formula
- generalize :: (FirstOrderFormula formula atom v, Atom atom term v) => formula -> formula

# Documentation

eval :: FirstOrderFormula formula atom v => formula -> (atom -> Bool) -> BoolSource

list_disj :: (Constants formula, Combinable formula) => Set formula -> formulaSource

list_conj :: (Constants formula, Combinable formula) => Set formula -> formulaSource

var :: forall formula atom term v. (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set vSource

Return all variables occurring in a formula.

fv :: forall formula atom term v. (FirstOrderFormula formula atom v, Atom atom term v) => formula -> Set vSource

Return the variables that occur free in a formula.

subst :: (FirstOrderFormula formula atom v, Term term v f, Atom atom term v) => Map v term -> formula -> formulaSource

generalize :: (FirstOrderFormula formula atom v, Atom atom term v) => formula -> formulaSource