Re: LOOM and PowerLoom

> > [Siddharth Goyal]
> > paper says that for LOOM, the engine is sound but not complete)

> [Thomas Russ]
> No.  It cannot be, since it implements first order logic.

Just to be pedantic, it depends on what you mean by "complete."  There
are complete theorem provers for first-order logic, meaning that if a
theorem is true in all models of a set of axioms, the prover will
eventually find a proof of that fact.  The Powerloom theorem prover
sacrifices completeness for speed, or at least that's my guess.

The sense in which, say, Peano arithmetic is incomplete is quite
different, even though Peano arithmetic is a first-order theory.  It
is still the case that a resolution theorem prover can prove any
statement that is _true in all models_ of Peano arithmetic; but the
_theory itself_ is incomplete because there are statements that we
have compelling reasons to believe the truth of but which are not true
in all models.  That is, there are nonstandard models in which these
statements are false.  The compelling reasons revolve around the fact
that if the statements are false then Peano arithmetic is inconsistent
and hence worthless (and it has no models at all).

I'm sure this makes these distinctions perfectly clear :)

                                             -- Drew McDermott