logic-classes-1.4.7: Framework for propositional and first order logic, theorem proving

Data.Logic.Harrison.Skolem

Synopsis

# 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

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

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

runSkolem :: SkolemT v term Identity a -> aSource

Run a computation in the Skolem monad.

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.