Data.Logic.ATP.Skolem

Prenex and Skolem normal forms.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Class of Skolem functions

class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where

Class of functions that include embedded Skolem functions

A Skolem function is created to eliminate an an existentially quantified variable. The idea is that if we have a predicate P[x,y,z], and z is existentially quantified, then P is only satisfiable if there *exists* at least one z that causes P to be true. Therefore, we envision a function sKz[x,y] whose value is one of the z's that cause P to be satisfied (if there are any; if the formula is satisfiable there must be.) Because we are trying to determine if there is a satisfying triple x, y, z, the Skolem function sKz will have to be a function of x and y, so we make these parameters. Now, if P[x,y,z] is satisfiable, there will be a function sKz which can be substituted in such that P[x,y,sKz[x,y]] is also satisfiable. Thus, using this mechanism we can eliminate all the formula's existential quantifiers and some of its variables.

Associated Types

type SVarOf function

Methods

toSkolem :: SVarOf function -> Int -> function

Create a skolem function with a variant number that differs from all the members of the set.

foldSkolem :: (function -> r) -> (SVarOf function -> Int -> r) -> function -> r

variantSkolem :: function -> Set function -> function

Return a function based on f but different from any set element. The result may be f itself if f is not a member of the set.

Instances

HasSkolem Function

showSkolem :: (HasSkolem function, IsVariable (SVarOf function)) => function -> String

prettySkolem :: HasSkolem function => (function -> Doc) -> function -> Doc

Skolem monad

type SkolemM function = StateT (SkolemState function) Identity

runSkolem :: IsFunction function => SkolemT Identity function a -> a

Run a pure computation in the Skolem monad.

type SkolemT m function = StateT (SkolemState function) m

State monad for generating Skolem functions and constants.

runSkolemT :: (Monad m, IsFunction function) => SkolemT m function a -> m a

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

Skolemization procedure

simplify :: IsFirstOrder formula => formula -> formula

Routine simplification. Like "psimplify" but with quantifier clauses.

nnf :: IsFirstOrder formula => formula -> formula

Negation normal form for first order formulas

pnf :: IsFirstOrder formula => formula -> formula

Prenex normal form.

skolems :: (IsFormula formula, HasSkolem function, HasApply atom, Ord function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term) => formula -> Set function

Extract the skolem functions from a formula.

askolemize :: (IsFirstOrder formula, HasSkolem function, Monad m, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, VarOf formula ~ SVarOf function) => formula -> SkolemT m function formula

Overall Skolemization function.

skolemize :: (IsFirstOrder formula, JustPropositional pf, HasSkolem function, Monad m, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, VarOf formula ~ SVarOf function) => (AtomOf formula -> AtomOf pf) -> formula -> StateT (SkolemState function) m pf

Skolemize and then specialize. Because we know all quantifiers are gone we can convert to any instance of IsPropositional.

specialize :: (IsQuantified fof, JustPropositional pf) => (AtomOf fof -> AtomOf pf) -> fof -> pf

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. For this reason we can safely convert to any instance of IsPropositional.

Normalization

simpdnf' :: (IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) => fof -> Set (Set fof)

Versions of the normal form functions that leave quantifiers in place.

simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, IsFirstOrder fof, Ord fof) => fof -> Set (Set fof)

Instances

data Function

A function type that is an instance of HasSkolem

Constructors

Fn String

Skolem V Int

Instances

Eq Function

Data Function

Ord Function

Read Function

Show Function

IsString Function

Pretty Function

IsFunction Function

IsFirstOrder Formula

HasSkolem Function

Unify (SkAtom, SkAtom)

type SVarOf Function = V

type UTermOf (SkAtom, SkAtom) = TermOf SkAtom

type Formula = QFormula V SkAtom

A first order logic formula type with an equality predicate and skolem functions.

type SkTerm = Term Function V

type SkAtom = FOL Predicate SkTerm

Tests

testSkolem :: Test