|
|
Mitch wrote:
> Charlie-Boo wrote:
> > Mitch wrote:
> > > You know what would be really cool, is if your system could be run in a
> > > competition against other theorem provers. I seem to recall that there
> > > are competitions every year at the big ATP conferences (CADE, FTP, CAV,
> > > etc.). To practice, and get an idea for the formats, download TPTP (a
> > > thousand problems for theorem provers, I think). (google to find them)
> >
> > The only ones I have ever seen are propositional calculus theorem
> > provers.
>
> Oh.
>
> > Even TPTP is propositional calculus, where they rig the
> > axioms to fit the theorem. Instead of expressing the halting problem
> > in general terms (a predicate that is not recursive), they hardcode "If
> > HP is solvable then . . ." into the axioms. Pure BS.
>
> TPTP presents many problems: some are propositional, most are higher
> order.
Example of a non-propositional calculus proof called for, please. I
believe they all use the same input format, which is Propositional
Calculus.
Also note that each problem comes with its own set of axioms - all set
up just for that problem. What do you think of that?
How would you like an axiomatic system that requires a new set of
axioms every time you asked it to prove something? I assume you are at
least sophisticated enough to know that this violates the definition of
an axiomatic system. It also violates the spirit - which is to distill
a theory down to a fixed finite set of axioms and rules from which all
of its conclusions can be derived.
Hardwiring a new set of axioms for every theorem to be proven is a
pointless exercise in fraud. It's called "TPTP". Run by a bunch of
professors, of course. The biggest bull-shitters in the world.
Essentially none of Computer Science has been formalized - not Program
Synthesis, Theory of Computation, Recursion Theory (other than to show
a similarity to e.g. Combinatory Logic - without producing the various
theorems produced by hand in texts), Incompleteness in Logic (Modal
Logic tries hard, but texts on Modal Logic still resort to informal
proofs of almost all Incompleteness theorems).
CBL formalizes all of this. The ARXIV paper shows most of this. Give
your favorite Computer Science theorem and proof, and I'll show you how
it is formally represented and manipulated in CBL.
> For all the problems there, they also supposedly have solutions (from
> many of the various provers) but I couldn't get it to work just now.
Oh! So you take back your statements about how easy it is to download
these wonderful systems and see what magical things they do?
> > If you ever see a competition for systems that prove Theory of
> > Computation theorems - for real - or Incompleteness in Logic theorems -
> > for real - not dittley propositional calculus problems (whose
> > optimization is a big research area that I have never gotten into),
> > then let me know. I would love to. I would have 0 competition.
>
> Excellent. Go for it.
Please let me know if anyone is truly interested in any of the above.
Not with pre-defined propositional calculus axioms hard-wired for each
theorem. Rather, an authentic formalization of any branch of Computer
Science. Really. Please do.
C-B
> Mitch
|
|