Subato

Resource Files

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.


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 distributive(){ return everywhere(x->x.distributiveTopLevel()); } default Logic distributiveTopLevel(){ //TODO //apply the two rules, //otherwise return the formula 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);} }
java
You are not logged in and therefore you cannot submit a solution.