Re: What happens if an assertion contradicts a rule?

Ah, consistency, a rarified and elusive goal :-)

First off, a tiny bit of theoretical background: in first-order logic,
consistency is undecidable.  That is, there is no general algorithm that -
given any logical theory (i.e., a set of assertions) - can determine whether
that theory is consistent or not.  Description logics are more restrictive in
expressivity to maintain decidability, which also makes consistency a
decidable property, it might still be very expensive to compute, though.

All that aside, given a specific theory such as the set of assertions you gave
below, it often is possible to find an inconsistency.  The problem for
PowerLoom is that such an inconsistency could be any goal P such that both P and
not P are derivable from the KB.  With any reasonably complex KB, the set of
possible P's to try becomes quickly very large plus you have to pay a
potentially large cost to try to prove each one of them.  Therefore, PowerLoom
doesn't try to do that.

However, not all hope is lost.  One way to deal with some aspect of this is to
use PowerLoom's forward inference machinery.  Since forward inference is an
exhaustive type of inference that infers everything that follows from
assertions and forward rules plus a few other limited inference strategies, it
has the flavor you need to find an inconsistency "somewhere" without knowing
exactly where to look.  For example, if you rewrite your rule below as a
forward-only rule with the =>> arrow, you can get what you want (CAVEAT, you
need the latest 4.0.1 snapshot for this example, which fixes a bug related to
inequality evaluation):

|= (defrule EXISTENCE-START-END
      (forall (?p ?s ?e)
         (=>> (and (= (EXISTENCE-START ?p) ?s)
                   (= (EXISTENCE-END   ?p) ?e))
              (< ?s ?e))))

|P|(FORALL (?p ?s ?e)
   (=>> (AND (= (EXISTENCE-START ?p) ?s) (= (EXISTENCE-END ?p) ?e))
        (< ?s ?e)))

|= (assert (THING-PREDICATOR t1))
|P|(THING-PREDICATOR T1)

|= (assert (= (EXISTENCE-START t1) 10))
|P|(= (EXISTENCE-START T1) sk05//10)

|= (assert (= (EXISTENCE-END   t1)  8))
|P|(= (EXISTENCE-END T1) sk06//8)

|= (run-forward-rules)
Warning: Retraction of `|P?|(< 10 8)' occurred in world `|WLD|40' which is marked monotonic.
Derived both TRUE and FALSE for the proposition `(< 10 8)'.
   Clash occurred in the meta inference cache for module `/PL-KERNEL-KB/PL-USER'.   One or more facts need to be retracted to eliminate the inconsistency.


In order to trigger the inconsistency, we needed to call `run-forward-rules'
explicitly, to chain all currently known assertions through all forward
rules.  The more localized just-in-time forward inference used during backward
chaining might not trigger the inconsistency depending on the kind of query
you asked.

Tom Russ also recently added some machinery that now allows you to find all
currently known inconsistent propositions via the following command (again,
only in the very latest 4.0.1 snapshot):

STELLA(12): (list-inconsistent-propositions)
(|P?|(< 10 8))

Btw, PowerLoom treats inconsistent propositions as unknown to allow it to keep
functioning even if some portions of the KB are inconsistent.

We also recently added machinery to keep justifications for such propositions,
and we should have commands soon so you can get explanations for them at the
user level (currently this is only possible programmatically or if
inconsistencies were derived during backward inference).

So, where to go from here?  It really depends on what you are doing, how large
your KB is, how important consistency is for you, etc.  You might code much of
your KB via forward rules to get the exhaustive checking all the time, or you
might have separate constraint rules or constraint queries that are in their
own module and only run once in a while as a kind of test suite on the KB.

I rarely find myself worrying about this which is probably the reason why this
area of PowerLoom is a bit underdeveloped.  Once a KB is reasonably large and
complex, it will be inconsistent, particularly if it is based on real data.
What's important at this point is that the system can keep functioning despite
such inconsistencies.

Consistency is a meta-property that to me is most useful when you do abductive
and hypothetical reasoning.  You make an abductive assumption but it leads to
an inconsistency with what you already know.  That's interesting and now you
have to make a decision what to do about that at which point you usually have
to go outside of logic to resolve the issue.

Anyway, I hope this wasn't too confusing,

Hans

--------------------------------------------------------------------------
Hans Chalupsky, PhD                     USC Information Sciences Institute
Project Leader, Loom KR&R Group         4676 Admiralty Way
<[email protected]>                          Marina del Rey, CA 90292
(310) 448-8745
--------------------------------------------------------------------------

>>>>> Oliver Uwira <[email protected]> writes:

> Hello everybody,
> I am trying to model the existence of things in time, where points in 
> time are to be simple integers.

> Specifically, I want to implement two functions representing the start 
> and end points of existence:

> (defconcept PREDICATOR)
> (defconcept THING-PREDICATOR (?p PREDICATOR))
			
> (deffunction EXISTENCE-START ((?p THING-PREDICATOR)) :-> (?t INTEGER))
> (deffunction EXISTENCE-END   ((?p THING-PREDICATOR)) :-> (?t INTEGER))

> Going from there, I want to make sure that the start point of existence 
> must always precede the end point of existence. In order to ensure this, 
> I added the following rule:

> (defrule EXISTENCE-START-END
>    (forall (?p ?s ?e)
>      (=>
>        (and
>          (= (EXISTENCE-START ?p) ?s)
>          (= (EXISTENCE-END   ?p) ?e)
>        )
>        (< ?s ?e)
>      )
>    )
> )

> However, this rule doesn't seem to prevent PowerLoom from accepting 
> assertions that contradict it:

> (assert (THING-PREDICATOR t1))
> (assert (= (EXISTENCE-START t1) 10))
> (assert (= (EXISTENCE-END   t1)  8))

> The last assertion contradicts above rule, but no error message pops up. 
> I wonder what is the correct approach for keeping a knowledge base 
> consistent.

> Many thanks in advance,
> Oliver Uwira
> _______________________________________________
> powerloom-forum mailing list
> [email protected]
> http://mailman.isi.edu/mailman/listinfo/powerloom-forum