Reasoning foundations
Evidence
Data that another procedure can use to check a result.
Definition
Evidence
Evidence records enough information for a stated checker to test a result.
The form depends on the result. A sat result can carry a model, an unsat result can carry a certificate, and a theorem can carry a proof term.
01
Example
The assignment a = true and b = false is evidence when evaluating it makes every clause true.
02
Important distinction
A log line saying 'success' reports an outcome but does not explain how to check it.
After reading this article, you should be able to
- Define Evidence in the sense used on this site.
- Match a model, certificate, or proof term to the result it can check.