| | | B.5.2 skolemize: Skolemize Quantified Formulas |
skolemize
In proving mode.
The command generates a single child state by skolemizing every suitable quantified formula (assumption or goal) of the current proof state according to the rules listed below. For every formula of the current state, the command looks for an applicable rule (there can be at most one) and, if such a rule exists, applies it to the state; i.e. a rule is applied at most once for every formula (for a repeated application of the rules, see the command decompose). If no rule is applicable at all, no child state is generated.
The applied rules are:
[E,a:T] ... |- ..., A[a/x], ...
~\/ T: [E] |- a:T
---------------------------------
[E] ... |- ..., /\ x in T: A, ...
[E,a:T] ..., A[a/x], ... |- ...
~\/ T: [E] |- a:T
---------------------------------
[E] ..., \/ x in T: A, ... |- ...
In both rules, a new skolem constant a is generated that does not occur in the current proof state and which in the child state replaces the variable x bound by the quantifier in the current state.
For better readability, the name of the skolem constant a is derived from the name of the bound variable x by appending some natural number subscript (x0, x1, ...) respectively by replacing an already existing subscript.
The effect of this command is actually subsumed by the effect of the command decompose. The only reason to apply flatten directly is to observe step-by-step how decompose produces its result.
| | | B.5.2 skolemize: Skolemize Quantified Formulas |