6 Rule formalism extended to support abduction

In RacerPro, Abox rules can be specified that are applied w.r.t. the autoepistemic semantics. In a nutshell this means the following: if for the variables in the rule body (precondition), some bindings withindividuals of the Abox can be found such that all instantiated query atoms of the body are entailed, then the assertion of the rule head (conclusion) is added to the Abox with variables instantiated appropriately (forward-chaining). All rules whose preconditions match the assertions of the Abox in the way just described are applied until nothing new can be added. The rule mechanism allows for a convenient augmentation of Aboxes with assertions. For details of the formalism see the nRQL User’s Guide. An example for such a rule is the following statement.

(define-rule (?x ?y has-sibling)  
  (and (?z ?x has-child)  
       (?z ?y has-child)  
       (?x human)))

The form (?x ?y has-sibling) is the head and the rest is the body.

Rules may also be specified as part of an OWL document in SWRL syntax (see Figure 12 for a graphical specification of SWRL rules in Protege).


PIC

Figure 12: Rules in Protege.


Rules are required because for some purposes, OWL is not expressive enough. Rather than just adding statements to the Abox whenever preconditions are satisfied as suggested above, in some cases it makes sense to just ask whether the head is entailed by an Abox (rules are applied in a backward-chaining way). This facility can also be used for computing what should be added to an Abox to make an assertion be entailed (abduction). Depending on the rule, this could involve the addition of new individuals to the Abox. In the following we present an example involving the detection of a pole-vault event.

(full-reset)  
 
(in-knowledge-base test)  
 
(define-primitive-role near)  
(define-primitive-role has-part)  
 
(disjoint pole bar)  
(disjoint pv-in-start-phase pv-in-turn-phase)  
 
(define-rule (?x ?y near)  
  (and (?z ?x has-part)  
       (?z ?y has-part)  
       (?x pole)  
       (?y human)  
       (?z pole-vault)  
       (?z pv-in-start-phase)))  
 
(define-rule (?x ?y near)  
  (and (?z ?x has-part)  
       (?z ?y has-part)  
       (?x bar)  
       (?y human)  
       (?z pole-vault)  
       (?z pv-in-turn-phase)))  
 
(instance p1 pole)  
(instance h1 human)

Given the statements in this knowledge base one can ask the following query.

(retrieve-with-explanation () (p1 h1 near) :final-consistency-checking-p t)

The answer is

(t (((:tuple)  
      (:new-inds IND-2)  
      (:hypothesized-assertions  
         (related IND-2 p1 has-part)  
         (instance IND-2 pole-vault)  
         (instance IND-2 pv-in-start-phase)  
         (related IND-2 h1 has-part)))))

The answer is t (as expected), and the result returned by RacerPro suggests that there is one way to achieve this answer. One new individual is required (IND-2). In addition, a set of hypothesized assertions to achieve the positive answer is indicated. Multiple ways to (positively) answer the query are possibly generated in other cases. If the optional keyword argument :final-consistency-checking-p t is used, RacerPro checks if the Abox would remain consistent if the hypothesized assertion were added to the Abox. The additional option :incremental-consistency-checking-p t might be more efficient in some cases (intermediate checks) but there is some overhead with multiple consistency checks.

Now, assume that there are some additional assertions added as in the following example.

(full-reset)  
 
(in-knowledge-base test)  
 
(define-primitive-role near)  
(define-primitive-role has-part)  
 
(disjoint pole bar)  
(disjoint pv-in-start-phase pv-in-turn-phase)  
 
(define-rule (?x ?y near)  
  (and (?z ?x has-part)  
       (?z ?y has-part)  
       (?x pole)  
       (?y human)  
       (?z pole-vault)  
       (?z pv-in-start-phase)))  
 
(define-rule (?x ?y near)  
  (and (?z ?x has-part)  
       (?z ?y has-part)  
       (?x bar)  
       (?y human)  
       (?z pole-vault)  
       (?z pv-in-turn-phase)))  
 
(instance p1 pole)  
(instance h1 human)  
(instance e1 pole-vault)  
(instance e1 pv-in-start-phase)  
(related e1 p1 has-part)  
(related e1 h1 has-part)

Given the statements in this knowledge base on can ask the query from above again.

(retrieve-with-explanation () (p1 h1 near) :final-consistency-checking-p t)

The answer is now:

(t (((:tuple) (:new-inds) (:hypothesized-assertions))))

This means, (p1 h1 near) would be added if the rule was applied in a forward-chaining way, i.e., no hypothesized assertions are required. The retrieve-with-explanation facility can also be used for explaining to a user what must be added to an Abox in order to positively answer a query.

Racer Systems has applied the abduction operator to media interpretation problems (image interpretation and natural language text interpretation). We offer consulting to support industrial application projects that could use these facilities.