module Data.Logic.Satisfiable
( satisfiable
, theorem
, inconsistant
, invalid
) where
import qualified Data.Set as Set
import Data.Logic.Classes.Atom (Atom)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), toPropositional)
import Data.Logic.Classes.Literal (Literal)
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Propositional (PropositionalFormula)
import Data.Logic.Classes.Term (Term)
import Data.Logic.Harrison.Skolem (SkolemT)
import Data.Logic.Instances.PropLogic ()
import Data.Logic.Normal.Clause (clauseNormalForm)
import qualified PropLogic as PL
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
satisfiable f =
do (clauses :: Set.Set (Set.Set formula)) <- clauseNormalForm f
let f' = PL.CJ . map (PL.DJ . map (toPropositional PL.A)) . map Set.toList . Set.toList $ clauses
return . PL.satisfiable $ f'
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
inconsistant f = satisfiable f >>= return . not
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
theorem f = inconsistant ((.~.) f)
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
invalid f = inconsistant f >>= \ fi -> theorem f >>= \ ft -> return (not (fi || ft))