FRD
Brief:
Intended as a "universal database of mathematical knowledge"
Jump To:
Parent Description
-
As Leibniz said, calculemus!
The idea is that real life problems
are reducible to computational problems, which are reducible to
mathematical problems.
Thus, Algorithmic Information Theory is
applicable, which says that if a set of mathematical problems
contains t-bits of information (Shannon entropy), and our program
for solving these problems contains less than t-bits of
information, then it is impossible to solve these problems from
these programs.
This is an example in itself of epistemic
reasoning deciding practical reasoning, for we know that it is
necessary to increase the Shannon entropy or rather Kolmogorov
complexity of our programs in order to have chance to solve more
problems.
The easiest practical method of achiving this is to
collect software that people have written.
We are working to mechanize this (
https://frdcsa.org/frdcsa/introduction/writeup.txt ) argument, at
least the deductive components) into agda at present.
We are still working to formalize the abductive component into an
argumentation schema for practical reasoning.
In order to increase the K-complexity of our systems, we are
developing a sequence of mathematical formal libraries which are
able to solve strictly more computational problems.
For instance,
databases of known computational complexity results could aid
algorithms for computing the resource complexity of various
programs generated by metaprogramming and/or program synthesis.
See also:
https://frdcsa.org/~andrewdo/writings/FRD.odp
https://frdcsa.org/~andrewdo/pioneer/wk1/frdcsa.pdf