# DeductionRule

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.