Resource Files

• exercise1090.zip
• .Logic.java
  Solution Template

In dieser Aufgabe verwenden wir einige Vorschau Eigenschaften 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 jetzt 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("unknown Logic class: "+this);
  }
}

Implementieren Sie die Methode zur Ersetzung von Implikationen in Disjunktionen nach der bekannten Umformung (A → B) wird zu (¬A ∨ B), indem Sie mit Hilfe der Methode everywhere eine Funktion, die Implikationen auf top-level Ebene in eine Disjunktion umwandelt.

Jetzt brauchen Sie also nicht mehr rekursiv in die Teilformeln zu schauen. Dieses macht die Methode everywhere dann für Sie.

package name.panitz.util; import java.util.function.Function; public interface Logic{ static record Var(String n) implements Logic{ public String toString(){return n;} } static record Neg(Logic f) implements Logic{ public String toString(){return "¬"+f;} } static record Implication(Logic l,Logic r) implements Logic{ public String toString(){return "("+l+"→"+r+")";} } static record And(Logic l,Logic r) implements Logic{ public String toString(){return "("+l+"∧"+r+")";} } static record Or(Logic l,Logic r) implements Logic{ public String toString(){return "("+l+"∨"+r+")";} } 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); } default Logic transformImplications(){ return everywhere(x->x.replaceTopLevelImplication()); } default Logic replaceTopLevelImplication(){ //TODO //implications get replaced //all other formulae will stay unchanged. return this; } default Logic and(Logic that){return new And(this,that);} default Logic or(Logic that){return new Or(this,that);} default Logic implication(Logic that){return new Implication(this,that);} default Logic neg(){return new Neg(this);} }