7.6 Bestimmung überflüssiger Voraussetzungen

Da jede Prämisse einzeln in die Felder der Datenstruktur, die das Venn-Diagramm repräsentiert, eingetragen wird, ist es sehr einfach möglich, zu prüfen, ob in bezug auf das gesamte Prämissensystem Prämissen redundant vorhanden sind.

Bei den Prämissen $a \sqcap b \sqsubseteq 0$ und $a \sqsubseteq 0$ ist z.B. $a \sqcap b \sqsubseteq 0$ völlig überflüssig. In ähnlicher Weise können auch partikuläre Prämissen behandelt werden.

In einem rekursiven Prozeß werden Enthaltenseinsbeziehungen der Prämissen untereinander geprüft.