AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug ~~Donate~~ Contacts

Soundness

Property

Summary

How well justified this one rule's claim is, or null where the
rule has no tier of its own and its set's applies. See
Soundness for what a tier is and is not.

Remarks

A set's tier is the minimum over its rules, so reading it as every rule's tier
understates most of them. All thirty sets in the registry declare
SoundUnderAssumptions, and one conditional rule
is enough to make that true of a set of a hundred. Asked per rule instead, most rules
written as data are Sound — they hold for
every complex argument, with nothing assumed — and the rest are conditional, in numbers
RuleAuthoringGuideTest measures rather than this comment quoting them. That
difference is invisible at set grain and is what a derivation needs in order to say why
a particular step was allowed.
null is the honest answer for a rule read off a switch: an arm
declares no tier, so it has none of its own, and inventing its set's would be a claim
the source does not make. A caller wanting the effective tier writes
rule.Soundness ?? set.Soundness, and the null is what tells it
that the second value is a fallback rather than a measurement.

AngouriMath

Table of contents

AngouriMath

Soundness