Komplexität einer Sequenz

Die Komplexität einer Sequenz (Logik) Φ⇒Δ ist definiert als die Summe der Anzahl der logischen Verknüpfungen (∧,∨,¬,→) aller Formeln in Φ∪Δ.
Dieser Wert nimmt in jedem Beweisschritt von der Wurzel zu den Blättern hin strikt ab, was die Terminierung der Beweissuche garantiert.