Re: Existence of proof verifiers: A comedy

On May 4, 3:08 am, Jan Burse <janbu...@xxxxxxxxxxx> wrote:
Charlie-Boo schrieb:

What I am saying is that DataBase Query Processing IS a problem of
using Logic, as is Program Synthesis and even Theory of Computation.
They talk about the obvious role of AND, OR, NOT in queries, but never
exploited that.  When you say it is off-topic. that is pointing out
that nobody came up with a general logical solution that uses
Predicate Calculus for the wff and Rules of Inference to reduce that
down to ANY file with any number of levels of hierarchy and any
logical expression at each level.

It seems that the deductive database/descriptive complexity
developments slipped your attention.

I am not saying that there is a wide base using
these approaches. But the approaches are already
there.

The problem is, that not so many exploits are possible
by logic. You can view FOL as a language, similar to
SQL. So when you change the language in the interface
to a database, this doesn't mean that you automatically
get a better execution.

What is done down in the execution, can be mostly
viewed as trading space for time. Thus when you have
an index, you are using more space, but you gain
some execution time.

What would be exactly the great gain by using FOL?

You are able to model your files and use them in place, including
files that do not follow the simple scheme of "main file pluse
indexes." You can apply the rules of logic to those FOL wffs. It
unites several branches of Mathematics/Computer Science: Program
Synthesis, Database Query Processing, even Theory of Computation.

C-B

Best Regards

.