Safe Haskell	None
Language	Haskell98

Data.Logic.Harrison.Skolem

Synopsis

Documentation

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

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

Just looks for double negatives and negated constants.

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

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

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

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

The Skolem monad transformer

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

The Skolem monad

runSkolem :: SkolemT v term Identity a -> a Source

Run a computation in the Skolem monad.

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

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

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

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 Source

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 Source

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 Source

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 Source

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.