Safe Haskell | None |
---|
Do satisfiability computations on any FirstOrderFormula formula by converting it to a convenient instance of PropositionalFormula and using the satisfiable function from that instance. Currently we use the satisfiable function from the PropLogic package, by the Bucephalus project.
- satisfiable :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool
- theorem :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool
- inconsistant :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool
- invalid :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m Bool
Documentation
satisfiable :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m BoolSource
Is there any variable assignment that makes the formula true? satisfiable :: forall formula atom term v f m. (Monad m, FirstOrderFormula formula atom v, Formula atom term v, Term term v f, Ord formula, Literal formula atom v, Ord atom) => formula -> SkolemT v term m Bool
theorem :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m BoolSource
Is the negation of the formula inconsistant?
inconsistant :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m BoolSource
Is the formula always false? (Not satisfiable.)
invalid :: forall m formula atom v term f. (FirstOrderFormula formula atom v, PropositionalFormula formula atom, Literal formula atom, Term term v f, Atom atom term v, Ord atom, Monad m, Eq formula, Ord formula) => formula -> SkolemT v term m BoolSource
A formula is invalid if it is neither a theorem nor inconsistent.