Data.Logic.Harrison.Skolem

Documentation

simplify :: (FirstOrderFormula fof atom v, Atom atom term v, Term term v f) => fof -> fof

lsimplify :: Literal lit atom => lit -> lit

Just looks for double negatives and negated constants.

nnf :: FirstOrderFormula formula atom v => formula -> formula

pnf :: (FirstOrderFormula formula atom v, Atom atom term v, Term term v f) => formula -> formula

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)

type SkolemT v term m = StateT (SkolemState v term) m

The Skolem monad transformer

type Skolem v term = StateT (SkolemState v term) Identity

The Skolem monad

runSkolem :: SkolemT v term Identity a -> a

Run a computation in the Skolem monad.

runSkolemT :: Monad m => SkolemT v term m a -> m a

Run a computation in a stacked invocation of the Skolem monad.

specialize :: forall fof atom v. FirstOrderFormula fof atom v => fof -> fof

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 pf

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 fof

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 pf

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 fof

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.