Results 1 to 2 of 2

Ausdruck in Konjunktive Normalform bringen

  1. #1 Reply With Quote
    Veteran Feuerstern's Avatar
    Join Date
    Sep 2007
    Posts
    602
    Hallo zusammen,

    ich versuche ein Prolog Programm zu schreiben, welches einen Ausdruck in die Konjunktive Normalform bringt. Ich kenne bisher den händischen Weg mithilfe der Warheitstabelle, allerdings vermute ich das der Weg in Prolog nicht die richtige Herangehensweise ist. Meine Idee war nun über die Äquivalentz Gesetze wie De Morgan und Distributivgesetze so umzuformen bis ich eine Konjunktive Normalform habe. Ich bin mir aber nicht sicher ob das tatsächlich der beste Weg ist und wie ich da am besten Vorgehe damit das auch zum Ziel führt.

    Habt ihr da eine Idee und den ein oder anderen Denkanstoß?

    Viele Grüße
    Feuerstern is offline

  2. #2 Reply With Quote
    Veteran Feuerstern's Avatar
    Join Date
    Sep 2007
    Posts
    602
    Ich hab es letztlich über folgenden Algorithmus gelöst:
    https://www.cs.jhu.edu/~jason/tutori...rt-to-CNF.html

    Code:
    // Any syntactically valid propositional formula φ must fall into
    // exactly one of the following 7 cases (that is, it is an instanceof
    // one of the 7 subclasses of Formula).
    
    If φ is a variable, then:
       return φ.
       // this is a CNF formula consisting of 1 clause that contains 1 literal
    
    If φ has the form P ^ Q, then:
       CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
       CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
       where all the Pi and Qi are disjunctions of literals.
       So return P1 ^ P2 ^ ... ^ Pm ^ Q1 ^ Q2 ^ ... ^ Qn.
    
    If φ has the form P v Q, then:
       CONVERT(P) must have the form P1 ^ P2 ^ ... ^ Pm, and
       CONVERT(Q) must have the form Q1 ^ Q2 ^ ... ^ Qn,
       where all the Pi and Qi are dijunctions of literals.
       So we need a CNF formula equivalent to
          (P1 ^ P2 ^ ... ^ Pm) v (Q1 ^ Q2 ^ ... ^ Qn).
       So return (P1 v Q1) ^ (P1 v Q2) ^ ... ^ (P1 v Qn)
               ^ (P2 v Q1) ^ (P2 v Q2) ^ ... ^ (P2 v Qn)
                 ...
               ^ (Pm v Q1) ^ (Pm v Q2) ^ ... ^ (Pm v Qn)
    
    If φ has the form ~(...), then:
      If φ has the form ~A for some variable A, then return φ.
      If φ has the form ~(~P), then return CONVERT(P).           // double negation
      If φ has the form ~(P ^ Q), then return CONVERT(~P v ~Q).  // de Morgan's Law
      If φ has the form ~(P v Q), then return CONVERT(~P ^ ~Q).  // de Morgan's Law
    
    If φ has the form P -> Q, then:
      Return CONVERT(~P v Q).   // equivalent
    
    If φ has the form P <-> Q, then:
      Return CONVERT((P ^ Q) v (~P ^ ~Q)).
    
    If φ has the form P xor Q, then:
      Return CONVERT((P ^ ~Q) v (~P ^ Q)).
    Allerdings musste ich den Algorithmus noch um die Fallunterscheidung ~(P->Q) erweitern. Äquivalenz und xor war für mein Projekt nicht gefragt, aber ich vermute dafür wäre dann auch noch eine Fallunterscheidung für das NOT nötig.
    Feuerstern is offline

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •