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/core-design-and-pipeline.org | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'docs/core-design-and-pipeline.org') diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index 823a24e..c81b58a 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -111,13 +111,18 @@ two of the ladder in decision 10: with every measure position demanded ground at unfolding; self recursion and mutual recursion are the same check; - bounded enumeration through =Between=; -- decidable negation and universals only over decidable quantifiers; +- decidable negation and universals over decidable quantifiers; - residuation: open membership returns as residual constraints - instead of failing the plan. - -Not yet present: symbolic discharge (algebraic proof of universals -over infinite domains), Rocq certificates as admission evidence, and -active constraint propagation over residue. Each arrives as a + instead of failing the plan; +- interval propagation over residue: contradictions fail, finite + integer ranges enumerate; +- symbolic discharge, first fragment: universals over infinite + domains decided by kind inclusion and interval entailment, with + refutations backed by counterexamples. + +Not yet present: symbolic discharge beyond the interval fragment +(algebraic identities of relations, arithmetic decrease measures) +and Rocq certificates as admission evidence. Each arrives as a strengthening of admission or planning; none changes the semantics of what is already admitted. -- cgit v1.2.3