|
|
Charlie-Boo wrote:
> I think that a lot of people conclude that something that they don't
> understand must be "advanced". It's also hard to understand
> gibberish.
The Greeks called all non-greeks "barbarians", this word (derived from
the Greek) an imitation of the babbling the non-Greeks were uttering.
> TPTP is a collection of theorems that serve as a benchmark for
> theorem-provers. Good idea, but the "axioms" are given with each
> theorem and are hard-wired for the theorem.
I don't see a problem with that at all. You have to define your
primitives somehow, how they relate to each other, before you can
attempt to prove something involving them. Otherwise, what are the
theorems actually about?
> For example, the Halting
> Problem axioms have as a primitive proposition "The Halting Problem
> is solvable."
Really? A provable proposition? That just sounds wrong. Since the
Halting problem isn't ..uh... solvable? I couldn't find anything like
that there:
http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Problems&Domain=COM&File=COM003+1.p
thru COM003+3.p are theorems, but COM003-1.p and COM003-2.p are labeled
as unsatisfiable.
> This is not at all general, would not generate
> anything but itself
TPTP doesn't have any inference rules, it is just a database of
formally written down theorems.
So I take your "would not generate anything but itself" as pretty much
a denial that any system out there can even apply the simplest modus
ponens. That's just silly.
> > > but they give you the (BS - hardwired for each theorem) axioms to make it
> > > easier for their
> > > professor friends
> >
> > so logical content is sometimes in axioms, sometimes in rules of
> > inference; there's an efficiency tradeoff.
>
> But if each theorem has its own axioms, is that an axiomatic system for
> proving these results?
proving many results including the example theorem?
> > >- which are also (wrongly) propositional calculus.
> >
> > no, the TPTP axioms are first order.
>
> Look at the Theory of Computation examples.
links up above. looks first order to me.
> > As advertisment, Otter/Mace is another excellent 1st order theorem prover.
> > (I can't remember of there is a program synthesis part (like there is
> > for nuPRL) but one can think of Mace (the finite model checker) as a
> > way of calculating (finite) models for first order sentences).
>
> Without examples, you have nothing (aside from warm and squishy.)
google otter
Mitch
|
|