Safe Haskell | None |
---|
- simplify :: (FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> fof
- lsimplify :: Literal lit atom => lit -> lit
- nnf :: FirstOrderFormula formula atom v => formula -> formula
- pnf :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) => formula -> formula
- functions :: forall formula atom f. (Formula formula atom, Ord f) => (atom -> Set (f, Int)) -> formula -> Set (f, Int)
- type SkolemT v term m = StateT (SkolemState v term) m
- type Skolem v term = StateT (SkolemState v term) Identity
- runSkolem :: SkolemT v term Identity a -> a
- runSkolemT :: Monad m => SkolemT v term m a -> m a
- specialize :: forall fof atom v. FirstOrderFormula fof atom v => fof -> fof
- skolemize :: forall m fof atom term v f pf atom2. (Monad m, FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pf
- askolemize :: forall m fof atom term v f. (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fof
- skolemNormalForm :: (FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Monad m, Ord fof, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pf
- skolem :: (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fof
Documentation
simplify :: (FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> fofSource
lsimplify :: Literal lit atom => lit -> litSource
Just looks for double negatives and negated constants.
nnf :: FirstOrderFormula formula atom v => formula -> formulaSource
pnf :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) => formula -> formulaSource
Convert to Prenex normal form, with all quantifiers at the left.
functions :: forall formula atom f. (Formula formula atom, Ord f) => (atom -> Set (f, Int)) -> formula -> Set (f, Int)Source
runSkolemT :: Monad m => SkolemT v term m a -> m aSource
Run a computation in a stacked invocation of the Skolem monad.
specialize :: forall fof atom v. FirstOrderFormula fof atom v => fof -> fofSource
Remove the leading universal quantifiers. After a call to pnf this will be all the universal quantifiers, and the skolemization will have already turned all the existential quantifiers into skolem functions.
skolemize :: forall m fof atom term v f pf atom2. (Monad m, FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pfSource
Skolemize and then specialize. Because we know all quantifiers are gone we can convert to any instance of PropositionalFormula.
askolemize :: forall m fof atom term v f. (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fofSource
I need to consult the Harrison book for the reasons why we don't |just Skolemize the result of prenexNormalForm.
skolemNormalForm :: (FirstOrderFormula fof atom v, PropositionalFormula pf atom2, Atom atom term v, Term term v f, Monad m, Ord fof, Eq pf) => (atom -> atom2) -> fof -> SkolemT v term m pfSource
We get Skolem Normal Form by skolemizing and then converting to Prenex Normal Form, and finally eliminating the remaining quantifiers.
skolem :: (Monad m, FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> SkolemT v term m fofSource
Skolemize the formula by removing the existential quantifiers and replacing the variables they quantify with skolem functions (and constants, which are functions of zero variables.) The Skolem functions are new functions (obtained from the SkolemT monad) which are applied to the list of variables which are universally quantified in the context where the existential quantifier appeared.