Safe Haskell | None |
---|---|
Language | Haskell98 |
Prenex and Skolem normal forms.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
- class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where
- type SVarOf function
- showSkolem :: (HasSkolem function, IsVariable (SVarOf function)) => function -> String
- prettySkolem :: HasSkolem function => (function -> Doc) -> function -> Doc
- type SkolemM function = StateT (SkolemState function) Identity
- runSkolem :: IsFunction function => SkolemT Identity function a -> a
- type SkolemT m function = StateT (SkolemState function) m
- runSkolemT :: (Monad m, IsFunction function) => SkolemT m function a -> m a
- simplify :: IsFirstOrder formula => formula -> formula
- nnf :: IsFirstOrder formula => formula -> formula
- pnf :: IsFirstOrder formula => formula -> formula
- skolems :: (IsFormula formula, HasSkolem function, HasApply atom, Ord function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term) => formula -> Set function
- 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
- 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
- specialize :: (IsQuantified fof, JustPropositional pf) => (AtomOf fof -> AtomOf pf) -> fof -> pf
- simpdnf' :: (IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) => fof -> Set (Set fof)
- 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)
- data Function
- type Formula = QFormula V SkAtom
- type SkTerm = Term Function V
- type SkAtom = FOL Predicate SkTerm
- testSkolem :: Test
Class of Skolem functions
class (IsFunction function, IsVariable (SVarOf function)) => HasSkolem function where Source #
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.
toSkolem :: SVarOf function -> Int -> function Source #
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 Source #
variantSkolem :: function -> Set function -> function Source #
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.
showSkolem :: (HasSkolem function, IsVariable (SVarOf function)) => function -> String Source #
Skolem monad
runSkolem :: IsFunction function => SkolemT Identity function a -> a Source #
Run a pure computation in the Skolem monad.
type SkolemT m function = StateT (SkolemState function) m Source #
State monad for generating Skolem functions and constants.
runSkolemT :: (Monad m, IsFunction function) => SkolemT m function a -> m a Source #
Run a computation in a stacked invocation of the Skolem monad.
Skolemization procedure
simplify :: IsFirstOrder formula => formula -> formula Source #
Routine simplification. Like "psimplify" but with quantifier clauses.
nnf :: IsFirstOrder formula => formula -> formula Source #
Negation normal form for first order formulas
pnf :: IsFirstOrder formula => formula -> formula Source #
Prenex normal form.
skolems :: (IsFormula formula, HasSkolem function, HasApply atom, Ord function, atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term) => formula -> Set function Source #
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 Source #
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 Source #
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 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. 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) Source #
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) Source #
Instances
A function type that is an instance of HasSkolem
Eq Function Source # | |
Data Function Source # | |
Ord Function Source # | |
Read Function Source # | |
Show Function Source # | |
IsString Function Source # | |
Pretty Function Source # | |
IsFunction Function Source # | |
IsFirstOrder Formula Source # | |
HasSkolem Function Source # | |
Monad m => Unify m (SkAtom, SkAtom) Source # | |
type SVarOf Function Source # | |
type UTermOf (SkAtom, SkAtom) Source # | |
type Formula = QFormula V SkAtom Source #
A first order logic formula type with an equality predicate and skolem functions.
Tests
testSkolem :: Test Source #