diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 09:59:59 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-12 17:56:10 -0300 |
| commit | e92c8e00290bab8db328058c437b471c0f1671a4 (patch) | |
| tree | f4ff85923298f70b7e66c3ec8e9e780bab784d7b /docs/core-design-and-pipeline.org | |
| parent | c3b4c7aee1f0d4beb078938d330e982e752927a1 (diff) | |
| download | SOL-e92c8e00290bab8db328058c437b471c0f1671a4.tar.gz SOL-e92c8e00290bab8db328058c437b471c0f1671a4.zip | |
algebraic identities of plus and times discharge symbolically
Diffstat (limited to 'docs/core-design-and-pipeline.org')
| -rw-r--r-- | docs/core-design-and-pipeline.org | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index c81b58a..eda5429 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -117,14 +117,15 @@ two of the ladder in decision 10: - 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. + domains decided by kind inclusion, interval entailment, and the + unit identities of the numeric relations, with refutations backed + by counterexamples. + +Not yet present: symbolic discharge beyond that fragment (richer +algebraic theories, 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. * What embedding means |