Vermeidung Irrelevanz einzelner atomarer Formeln

[jvoigtlaender]

Bei den Semantik-Aufgaben (mindestens denen zu Wahrheitstafeln) wäre es gut, Formeln wegzufiltern, deren Wert gar nicht von allen atomaren Formeln abhängt. Zum Beispiel (C => C) <=> (¬B ∧ (A ∨ D)).

Das Kriterium wäre: Für jede atomare Formel X gilt, die Gesamtformel ist nicht semantisch äquivalent zur Version, die erhalten wird, indem jedes Vorkommen von X durch ¬X ersetzt wird.