Aussagenlogische Formel: Ausmultiplizieren von Und und Oder

In dieser Aufgabe verwenden wir einige Preview Features aus Java 15.

Gegeben sei ein Datentyp für aussagenlogische Formeln.

public interface Logic{
  static record Var(String n) implements Logic{}
  static record Neg(Logic f) implements Logic{}
  static record Implication(Logic l,Logic r) implements Logic{}
  static record And(Logic l,Logic r) implements Logic{}
  static record Or(Logic l,Logic r) implements Logic{}

Innerhalb der Schnittstelle für logische Formeln gibt es zusätzlich eine Methode, die in der Lage ist, alle Teilformeln in der dargestellten Formel durch eine Funktionsanwendung zu ersetzen:

  default Logic everywhere(Function<Logic,Logic> f){
    var result = f.apply(this);
    if (result instanceof Neg n) return f.apply(new Neg(n.f.everywhere(f)));
    if (result instanceof Or n) return  f.apply(new Or(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof And n) return f.apply(new And(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Implication n) return f.apply(new Implication(n.l.everywhere(f),n.r.everywhere(f)));
    if (result instanceof Var v) return v;
    throw new RuntimeException("unhandled Logic class: "+this);
  }
}

Implementieren Sie eine Methode, die die folgende Umwandlungen der Distributivgesetze auf toplevel Ebene macht: A,B,C seien dabei beliebige Teilformeln.

• (A ∧ B) ∨ C wird zu (A ∨ C) ∧ (B ∨ C)
• C ∨ (A ∧ B) wird zu (C ∨ A) ∧ (C ∨ B)

Mit Hilfe der Methode everywhere erhalten Sie eine Umformung in eine logisch äquivalente Formel, in der alle Disjunktionen unterhalb von Konjunktionen stehen.

Zusammen mit den Aufgaben, Implikationen durch Disjunktionen zu ersetzen und die Negation nach innen zu verschieben, können Sie so die Formel in eine konjunktive Normalform umwandeln. Dieses wird für ein automatisches Beweisverfahren der Resolution benötigt.