Ideas 20180609

Proof and Computation

1. How Logic can be special Computation.

   1. A computation(trace) is a proof.
   2. An usual computation is straight forward, a proof needs searching.

2. Descriptive power and computation

   • If something is written as relations. But we can write a program that output same result, and more quick.
   • If the program was slow, the proving process will be slow. Especially proving is undecidable.
   • It is dubious that Logic's descriptive power is high.

3. What is good for Logic?

   • if Rel(p,x,y) == p(x,y), this may be the relation of abstract and concrete.
   • We can consider the all proofs. It is also the good point.

4. For example in image recognition, given a picture a1, ML can show a1 is p in probability q, where p is a tag.

   • This can be written as p(a1, q) and Rel(p, a1, q). The concept p may be predicate and term. The concept interchangeable is great point, I think.

5. Another approach is investigate the proof search elimination.

☕️