EML proof-search evidence
Law surfaces change what the loop may promote.
This lab visualizes the bounded EML constructor corpus. The same normalized rows are checked first under the base EML laws, then under the stronger bidirectional law surface. The remaining review rows stay visible because a semantic law cannot erase a failed positivity obligation.
L_base includes: log(exp(a)) = a
L_bi = L_base union { forall a, exp(log(a)) = a }
Loading
...
Reading the generated artifact.
Pipeline
The counts below are generated from the same local report as the tutorial. The important movement is not raw count. It is the split between symbolic inverse obligations and positivity obligations.
Two law surfaces
The base surface accepts only the direction already in the packet. The stronger surface adds the converse direction as an explicit premise.
Base
log(exp(a)) = a
... promoted.
BiLaws
log(exp(a)) = a
forall a, exp(log(a)) = a
... promoted.
Rows by selected surface
Toggle the law surface and filter by target. Promotion means the row passed the recorded qNS, proof, and obligation gates for this bounded corpus.
| Target | Expression | Status | Obligations |
|---|
Remaining blockers
These are not failures of the law-surface switch. They are rows where a logarithm-side domain obligation remains false in the bounded interval evidence.
How to read the result
Standard reading. Under the bounded corpus, selecting the BiLaws surface increases promoted target-consistent normalized rows from 13 to 20 of 22. The two non-promoted rows remain in review because the positive-value interval obligation is not discharged.
Plain English. Adding the missing inverse law lets the checker reuse more formula shapes, but the checker still refuses formulas whose logarithm inputs are not known to stay positive.