DeductionRule

From OpenCog
Jump to: navigation, search

The DeductionRule in PLN is an inference rule that implements the general notion of the "cut rule" from the theory of sequent calculus or "natural deduction". That is, the cut rule states that

A ==> B
B ==> C
--------
A ==> C

In the case where the arrow is an ImplicationLink, this just states that if A implies B and B implies C, then A implies C. Similarly, if the arrow is an InheritanceLink, the cut is just the deduction that if A is a B and B is a C then A is a C. Likewise for PartOfLink and SubsetLink.

The general case

All of the examples given above can be understood to be a special case of an EvaluationLink. Thus, the cut rule allows the deduction that if

EvaluationLink
    PredicateNode "foo"
    ListLink
       Atom A
       Atom B

and that

EvaluationLink
    PredicateNode "foo"
    ListLink
       Atom B
       Atom C

then

EvaluationLink
    PredicateNode "foo"
    ListLink
       Atom A
       Atom C


Note that exactly the same PredicateNode appears in all three. For the examples, "foo" would then be implication, inheritance, part-of and subset.

In PLN

The Deduction Rule in PLN can be initialised so that it can work on any underlying directed link type. Of course, it may not make sense for all links. InheritanceLinks and ImplicationLinks are those most frequently templated.

DeductionRule on ImplicationLinks

Note that revision isn't implemented, so just look at the secondary truth values.

(define AB (ImplicationLink
  (ConceptNode "A")
  (ConceptNode "B")
  (stv 1 0.7)))
(define BC (ImplicationLink
  (ConceptNode "B")
  (ConceptNode "C")
  (stv 1 0.7)))

(pln-bc (ImplicationLink
  (ConceptNode "A") (ConceptNode "C")) 200)
(ImplicationLink (ConceptNode "A") (ConceptNode "C"))

====>

(ImplicationLink
  (mtv (stv 0 0)
       (vh "CONTEXTUAL" 82).(stv 1 0))
  (ConceptNode "A") (ConceptNode "C"))

i.e. the resulting TV is <1,0>. If I add:

(ConceptNode "A" (stv 1 0.7))

Then it gets TV <1,1>.

(define AB (ImplicationLink
  (ConceptNode "A") (ConceptNode "B")
  (stv 0.7 0.7)))
(define BC (ImplicationLink
  (ConceptNode "B") (ConceptNode "C")
  (stv 0.7 0.7)))
(ConceptNode "A" (stv 0.7 0.7))

(pln-bc (ImplicationLink
  (ConceptNode "A") (ConceptNode "C")) 200)
(ImplicationLink
  (ConceptNode "A") (ConceptNode "C"))

======>

(ImplicationLink
  (mtv (stv 0 0)
       (vh "CONTEXTUAL" 82).(stv 0.48999998 1))
  (ConceptNode "A" (stv 0.69999999 0.69999999))
  (ConceptNode "C"))

Without A, it gets <0.48999998, 0>

These results are due to the count/confidence formula requiring the count of A:

nAC = IndependenceAssumptionDiscount * nA * nBC / max(nB, min_count);

The Deduction formula for strength also includes the TV of A, B, and C.

IF: max((sA+sB-1)/sA, 0) <= sAB<= min(1, sB/sA) AND max((sB+sC-1)/sB, 0) <= sBC <= min(1, sC/sB),

   sAC = [sAB*sBC + ((1-sAB)(sC - sB*sBC))/(1-sB)]

ELSE:

   sAC = 0

END

Note for the edge case sB = 1, it necessarily follows that sAC = sC if sC = sBC or 0 otherwise.