PowerLoom is the successor to the Loom knowledge representation system

Oliver Uwira | 13 Apr 2011 11:14

What happens if an assertion contradicts a rule?

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)
     )
   )
)

(Continue reading)

headers

Hans Chalupsky | 16 Apr 2011 04:28

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)

(Continue reading)