From 7aacf596d73cc74eb9af381a72723b50b4069e30 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 00:35:33 -0300 Subject: symbolic discharge: universals over infinite domains decided by intervals --- docs/vm.org | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'docs/vm.org') 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 -- cgit v1.2.3