Safe Haskell	None
Language	Haskell98

Data.Logic.Satisfiable

Description

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.

Synopsis

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 Bool Source

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 Bool Source

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 Bool Source

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 Bool Source

A formula is invalid if it is neither a theorem nor inconsistent.