NOTE.md

Evidence in constructive logic and statistics

In constructive logic, a proof is an evidence about the truth of a proposition, in probability theory, we also have evidences, just the evidence are not decisive, but only changing we degree of belief of the proposition.

We need a calculus of evidences.

• Is Bayes networks a calculus of evidences?

  • We might observe more { A: ..., B: ... } or { A: ... }.

    If we view evidence as observing more and more objects, what is the form of direct evidence of a conditional proposition B -> A, which increase P(A | B)?

    Is B merely a space for indexing, and evidence of A is evidence of a dependent type?

  • Think about Polya's book, it seems has more complicate evidences.

    If we are not sure about A, but we have proof of A -> B and proof of B, are't these proofs evidence of A?

    The above inference is an abduction, so evidence with uncertainty is constructed by abduction and induction?

• A database of evidences.

  • Like the PLANNER language?

• It seems logic is the key, which can connect many domain of study.

  • type theory.
  • probability.
  • computation -- SAT solver.