diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/vm.org | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/docs/vm.org b/docs/vm.org index 446cee2..a51b85a 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -96,10 +96,18 @@ open goals cannot happen. =Exists= lowers to a conjunction at loading, since query variables are existential already; its =variable:= is renamed apart so the scope cannot be forged. =ForAll= runs when its quantifier is -decidable: every solution of the quantifier must satisfy the body. A -universal over an infinite domain is a non total plan, rejected, as -decision 10 requires. Variables that live only under a universal are -not answer variables. +decidable: every solution of the quantifier must satisfy the body. +Variables that live only under a universal are not answer variables. + +A universal over an infinite domain is never enumerated. It gets one +chance at symbolic discharge: when quantifier and body both read as +kind and interval constraints over the quantified variable, the +engine decides entailment algebraically. Every natural is at least +zero: proven. Not every integer is: refuted, and the refutation is +backed by a concrete counterexample. Every integer is a rational: +proven, which is decision 12's subtype inclusion decided +symbolically. A universal outside that fragment is a non total plan, +rejected, as decision 10 requires. * Membership criteria as domains |