Review Note

Wie ist die Cut-Ableitbarkeit definiert?

Cut-Ableiten = Wiederholtes Anwenden der Schnittregel
Sei X eine Klauselmenge. Cut-Ableitbarkeit ist induktiv definiert:
A: Wenn K in X, so K aus X cut-ableitbar
S: Wenn K1 und K2 aus X cut-ableitbar und Cut(K1, K2, p_i, K), so K aus X cut-ableitbar.
Schnittregelabschluss: C(X)={K | K aus X cut-ableitbar}