Skip to content
Commit dc570d21 authored by Christoph Schwering's avatar Christoph Schwering
Browse files

Fixed: KnowledgeBase::BuildSpheres() omitted last pl-cons sphere.

A sphere with index p is plausibility consistent when for all
conditionals with antecedent alpha,
  LB(pl(alpha)) >= p iff UB(pl(alpha)) >= p,
where [L|U]B(pl(alpha) stands for "lower/upper bound of plausibility
of alpha."

LB(pl(alpha))>=p iff sound entailment returns consistency for sphere p.
UB(pl(alpha))>=p iff compl entailment returns consistency for sphere p.

Suppose at sphere p
* the sound entailment returns "might be consistent",
* the compl entailment returns "might be inconsistent".
Then LB(pl(alpha)) = p, but UB(pl(alpha)) > p.

Hence p is the last plausibility-consistent sphere. That is, p must be
added to the system of spheres, and then we skip over the next ones
until the last one, which is again added.

The bug was that sphere p was already skipped. That is, instead of
treating sphere p as the last plausibility-consistent one, it was
treated like the first plausibility-inconsistent one.
parent 76d4bc0c
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment