KI

Sven Eric Panitz

Kapitel 3 Logik

Oh Seifenblase, Oh Seifenblase,
In dir spiegelt sich ein kleiner Hase
Du leuchtest in allen Farben so bunt
In dir spiegelt sich auch ein kleiner Hund

• Wirklich interessante Gedichte sind nicht unbeliebt bei Leuten mit guten Geschmack.
• Keine moderne Poesie ist frei von einer gewissen Schwülstigkeit.
• Alle Deine Gedichte sind nun mal über Seifenblasen.
• Schwülstige Poesie ist nicht beliebt bei Leuten mit einen gewissen Geschmack.
• Kein älteres Gedicht beschäftigt sich mit Seifenblasen.

3.1 Aussagenlogik

3.1.1 Syntax

• $S\subset \mbox{For}_S$
• wenn $x\in \mbox{For}_S$ dann auch $\neg x \in \mbox{For}_S$
• wenn $x\in \mbox{For}_S$ und $x\in \mbox{For}_S$ dann auch $(x\rightarrow y)\in \mbox{For}_S$

3.1.2 Semantik

• $A$ ist eine Tautologie (allgemeingültig) gdw. für alle Interpretationen $I$ gilt: $w_I(A)=W$.
• $A$ ist ein Widerspruch (widersprüchlich, unerfüllbar) gdw. für alle Interpretationen $I$ gilt: $w_I(A) = F$.
• $A$ ist erfüllbar (konsistent) gdw. es eine Interpretationen $I$ gibt mit: $w_I(A)=W$.
• ein Modell für eine Formel $A$ ist eine Interpretation $I$ mit $w_I(A) = W$.

Aufgabe 3

• ``Abendrot Schlechtwetterbot'' kann man übersetzen in \\ $\mbox{Abendrot} \impl \mbox{Schlechtes\_Wetter}$. Diese Aussage ist weder Tautologie noch Widerspruch, aber erfüllbar.
• ``Wenn der Hahn kräht auf dem Mist, ändert sich das Wetter oder es bleibt wie es ist.'' kann man übersetzen in \\ $\mbox{Hahn\_kraeht\_auf\_Mist} \impl (\mbox{Wetteraenderung} \vee \neg \mbox{Wetteraenderung})$. \\ Man sieht, dass das eine Tautologie ist.

• $A\wedge A\leftrightarrow A$ (Idemtpotenz)
• $A\vee A\leftrightarrow A$ (Idemtpotenz)
• $ (A\wedge B)\wedge C \leftrightarrow A\wedge (B\wedge C)$ (Assoziativität)
• $ (A\vee B)\vee C \leftrightarrow A\vee (B\vee C)$ (Assoziativität)
• $A\wedge B \leftrightarrow B\wedge A$ (Kommutativität)
• $A\vee B \leftrightarrow B\vee A$ (Kommutativität)
• $A\wedge (B\vee C)\leftrightarrow (A\wedge B)\vee (A\wedge C)$ (Distributivität)
• $A\vee (B\wedge C)\leftrightarrow (A\vee B)\wedge (A\vee C)$ (Distributivität)
• $A\wedge(A\vee B)\leftrightarrow A$ (Absorption)
• $A\vee(A\wedge B)\leftrightarrow A$ (Absorption)
• $\neg\neg A\leftrightarrow A$ (Doppelnegation)
• $\neg(A\wedge B)\leftrightarrow \neg A\vee \neg B$ (de Morgan)
• $\neg(A\vee B)\leftrightarrow \neg A\wedge \neg B$ (de Morgan)

3.1.3 Kalküle

Kalkül des natürlichen Schließens

• $A_1=\{(A\rightarrow(B\rightarrow A))|A,B \in \mbox{For}_S\}$
• $A_2=\{(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A \rightarrow C)))|A,B,C \in \mbox{For}_S\}$
• $A_3=\{((A\rightarrow B )\rightarrow(\neg A\rightarrow \neg B))|A,B \in \mbox{For}_S\}$

• $A_i\in M$
• oder $A_i\in Ax$
• oder es existieren $j,k<i$ mit $A_j=(A_k\rightarrow A_i)$

Der Resolutionskalkül

• ersetze sukzessive Teilformeln der Gestalt $\neg\neg A$ durch $A$, $\neg(A\vee B)$ durch $(\neg A \wedge \neg B)$, $\neg(A\wedge B)$ durch $\neg A\vee \neg B$ bis keine der Umformungen mehr möglich ist.
• dann ersetze Teilformeln der Gestalt $(A\vee(B\wedge C))$ durch $(A\vee B)\wedge(A\vee C)$ und $((B\wedge C)\vee A)$ durch $(B\vee A)\wedge(C\vee A)$ bis keine der Umformungen mehr möglich ist.

3.1.4 Implementierung

package name.panitz.ki
case class Atom(name:String) extends Formel{
  override def toString()=name}
case class Not(e1:Formel) extends Formel{
  override def toString()="¬"+e1.toString}
case class Impl(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" -> "+e2.toString+")"}
case class And(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" /\\ "+e2.toString+")"}
case class Or(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" \\/ "+e2.toString+")"}

abstract class Formel{
  def eliminateImpl():Formel={
   this match {
    case Atom(_)  => this
    case Not(x)   => Not(x.eliminateImpl)
    case And(x,y) => And(x.eliminateImpl,y.eliminateImpl)
    case Or(x,y)  => Or(x.eliminateImpl,y.eliminateImpl)
    case Impl(x,y)=> Or(Not(x.eliminateImpl),y.eliminateImpl)
   }
  }

  def negationToInner():Formel={
   this match {
    case Atom(_)       => this
    case Not(Atom(x))  => this
    case Not(Not(x))   => x.negationToInner
    case Not(And(x,y)) => Or(Not(x),Not(y)).negationToInner
    case Not(Or(x,y))  => And(Not(x),Not(y)).negationToInner
    case And(x,y)      => And(x.negationToInner,y.negationToInner)
    case Or(x,y)       => Or(x.negationToInner,y.negationToInner)
   }
  }

  def makeConjunctions():Formel={
   this match {
    case Atom(_)       => this
    case Not(x)        => this
    case Or(And(x,y),z)=> And(Or(x,z),Or(y,z)).makeConjunctions
    case Or(x,And(y,z))=> And(Or(x,y),Or(x,z)).makeConjunctions
    case Or(x,y) 
      => val x1 =x.makeConjunctions
         val y1 =y.makeConjunctions
         x1 match { 
           case And(_,_) => Or(x1,y1).makeConjunctions
           case _        => y1 match {
                           case And(_,_) => Or(x1,y1).makeConjunctions
                           case _        => Or(x1,y1)
	                 }
         }
    case And(x,y)      => And(x.makeConjunctions,y.makeConjunctions)
   }
  }

  def toCNF():Formel=eliminateImpl.negationToInner.makeConjunctions

  import scala.collection.mutable.HashSet
  import scala.collection.mutable.Set
  def conjunctionSet():Set[Formel]={
    val result=new HashSet[Formel]()
    this match {
      case And(e1,e2) => result++= e1.conjunctionSet;
                         result++= e2.conjunctionSet;
      case e => result+= e
    }
    result
  }

  type Klausel=Set[Formel]
  def disjunctionSet():Klausel={
    val result=new HashSet[Formel]()
    this match {
      case Or(e1,e2) => result++= e1.disjunctionSet;
                        result++= e2.disjunctionSet;
      case e => result+= e
    }
    result
  }

  def cnf():List[Klausel]=
    (for (val f<- toCNF.conjunctionSet.elements) 
       yield f.disjunctionSet).toList

  def negated()= this match { case Not(x) => x
                              case y      => Not(y)}

}

package name.panitz.ki
object Resolution{
  import scala.collection.mutable.Set
  import scala.collection.mutable.HashSet
  type Klausel=Set[Formel]

  def resolvable(xs:Klausel,ys:Klausel)=
    xs.exists((x)=>ys.exists((y)=>y.negated==x))

  def resolve(xs:Klausel,ys:Klausel)={
    val result=new HashSet[Formel]()
    for (val x<-xs.elements;!ys.exists((y)=>y==x.negated)) result+=x
    for (val y<-ys.elements;!xs.exists((x)=>y==x.negated)) result+=y
    result
  }

  def resolution(xsP:List[Klausel])={    
    var xs=xsP
    var zs=xsP
    while (!zs.isEmpty && !zs.exists((x)=>x.size==0)){
      val ks=
       for (val x<-xs;val y<-zs;resolvable(x,y)) yield resolve(x,y)
       
      zs=ks.toList
      xs= xs ::: zs
    }
    xs
  }

  def proof(a:Formel):List[Set[Formel]]=proof(List(),a)
  def proof(ms:List[Formel],a:Formel):List[Set[Formel]]={
    var clauses=List[Set[Formel]]()      
    for (val m<-ms) clauses = m.cnf ::: clauses
    clauses = Not(a).cnf ::: clauses
    resolution(clauses)
  }
}

package name.panitz.ki
object TestFormel extends Application{
  val ax1:Formel = Impl(Atom("A"),Impl(Atom("B"),Atom("A")))
  Console println ax1
  Console println ax1.toCNF
  Console println Resolution.proof(ax1) 

  val ax2=Impl(Impl(Atom("A"),Impl(Atom("B"),Atom("C")))
              ,Impl(Impl(Atom("A"),Atom("B")),Impl(Atom("A"),Atom("C"))))
  Console println ax2
  Console println ax2.toCNF
  Console println Resolution.proof(ax2) 


  val ax3=Impl(Impl(Atom("A"),Atom("B")),Impl(Not(Atom("B")),Not(Atom("A"))))
  Console println ax3
  Console println ax3.toCNF
  Console println Resolution.proof(ax3) 
}