Re: LOOM and PowerLoom

Just adding my two cents here:

>>>>> Drew McDermott <drew.mcdermott <at> yale.edu> writes:

>> > [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.

As Drew clarified , standard first order logic is only
semi-decidable, that is, if a statement is a theorem, an algorithm
such as a resolution theorem prover will find a proof for it, even
though for some theorems it might take a very very long time; however,
when applied to some non-theorems, the algorithm will never terminate
(hence, only "semi"-decidable).  However2, given the worst-case
exponential complexity for the decidable portion, even a complete
algorithm as used by a resolution prover will be practically
incomplete, since, for some theorems it will not terminate in your
life time.

As Drew guessed correctly, PowerLoom's inference engine is not
complete in this sense.  PowerLoom uses a natural deduction inference
engine, and, for example, one of the inference rules we do not
currently implement is reasoning by cases (A->C, B->C, AvB |- C).

What we should do is to either characterize these areas of
incompleteness more carefully, or, extend PowerLoom's inference engine
to be complete (in the sense a resolution prover is complete) for
knowledge bases that do not go beyond standard first order logic.  The
main reason why this hasn't happened yet, is that it is of relatively
little practical value for the overall system, and would primarily
make it easier for us to write certain papers about PowerLoom.

While I am at it: in my opinion, a KR&R system such as PowerLoom
occupies a very different space compared to theorem provers such as,
for example, Otter (or Prover9).  What a KR system should do well is
to allow you to represent potentially large amounts of knowledge
easily and with minimal restrictions.  The job of the inference engine
is then to efficiently make the expected inferences that are more or
less "just around the corner".  That is, you should generally not be
surprised by the inferences your KR system makes.  If a particular
expected inference requires a long reasoning chain for the system to
find, you probably should add some rules or model your KB differently.
This is very different from the space that theorem provers address,
which generally try to prove deep theorems - say Fermat's Last Theorem
- from a small number of axioms or assumptions.  Turning that around,
completeness in the sense described above isn't really that important
for a KR&R system such as PowerLoom, what's much more important is
completeness in the sense of finding all the inferences one should
"reasonably expect" in "reasonable time".  The problematic part with
this last statement is that this "reasonable" space is difficult to
define or formalize.

Hans

--------------------------------------------------------------------------
Hans Chalupsky, PhD                     USC Information Sciences Institute
Project Leader, Loom KR&R Group         4676 Admiralty Way
<hans <at> isi.edu>                          Marina del Rey, CA 90292
(310) 448-8745
--------------------------------------------------------------------------

> 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

> _______________________________________________
> powerloom-forum mailing list
> powerloom-forum <at> isi.edu
> http://mailman.isi.edu/mailman/listinfo/powerloom-forum