 Grove’s sphere systems can also be used for contraction. In sphere-based contraction by \(p\), those elements of \([\neg p]\) are added that belong to the closest sphere around \([K]\) that has a non-empty intersection with \([\neg p]\). The procedure is shown in Diagram 4. Sphere-based contraction corresponds exactly to transitively relational partial meet contraction.