Not logged in. · Lost password · Register

Matombo
Member since Aug 2014
30 posts
Subject: Prenex normal form
Übung 10 auufgabe 2 steht was von prenex normal form
ich kann das aber in den folien nirgens finden, müssen wir das können?
Shadow992
Member since Jan 2014
290 posts
Quote by Matombo:
Übung 10 auufgabe 2 steht was von prenex normal form
ich kann das aber in den folien nirgens finden, müssen wir das können?

Das ist nichts anderes als, dass du alle Quantoren vor die ganze Formel schreibst. Im Grunde kannst du "einfach so" die Quantoren rausziehen an den Anfang, musst aber eventuell Variablen-Kolisionen auflösen (also einfach Variablen umbenennen, wenn sie denselben Namen hätten). Die Pränex-Normalform ist Voraussetzung für die Skolemisierung, weswegen man das defintiv für die Klausur braucht (vorausgesetzt Skolemization kommt in der Klausur in irgendeiner Form dran).

Wikipedia dazu fasst das auch sehr schön und kurz zusammen:
https://de.wikipedia.org/wiki/Pr%C3%A4nexform
This post was edited on 2017-02-12, 16:39 by Shadow992.
Matombo
Member since Aug 2014
30 posts
in der aufgabe verändern sich die quantoren aber von exists zu forall quantoren
wikipedia vertät mir das liegt am ->, wüssen wir die regeln können?
This post was edited 2 times, last on 2017-02-12, 16:41 by Matombo.
Shadow992
Member since Jan 2014
290 posts
Quote by Matombo:
in der aufgabe verändern sich die quantoren aber von exists zu forall quantoren
wikipedia vertät mir das liegt am ->, gibts da noch mehr regeln?

Die Musterlösung ist echt nicht "super durchsichtig", da werden ziemlich viele Schritte auf einmal gemacht.
Aber du kannst  natürlich ForAll und Exists ineinander umwandeln, es gelten folgende Äquivalenzen:
1) ForAll.X(~P(X)) = ~Exists.X(P(X))
2) ~ForAll.X(P(X)) = Exists.X(~P(X))
Matombo
Member since Aug 2014
30 posts
äh jah nur anders: https://en.wikipedia.org/wiki/Prenex_normal_form#Implication
das -> wir aufgelöst dann die exists zu forall regel angewand und dann das -> wieder eingefügt oda so

noch ne andre frage: im 2. schritt der musterlösung werden bei der skolomization die foralls vor den exists quantoren entfernt, darf man das deswegen machen weil die exists quantoren im nächsten schritt auch zu voralls umgewandelt werden? (ake hängen die exists quantoren von den vorherstehenden forallquantoren ab? aka man kann sie nur mit funktioner der form g(x,y,z) ersetzen?
Jazzpirate
Member since Oct 2016
806 posts
Ähm, die Lösung ist nur in der Form drin, weil ich die vor 3 jahren schonmal getext und noch rumfliegen hatte - der KNF-Algorithmus aus den slides kommt ohne Normalformen aus. Entsprechend müsst ihr Pränexen auch nicht prinzipiell können, geschweige denn die Implikationsregel (ich vergess die auch jedes mal wieder und leite sie wieder neu her :D ). Alles was ihr können müsst ist EINE variante aus ner FOL-Formel die Klauseln für Resolution zu erzeugen ;-)
Jazzpirate
Member since Oct 2016
806 posts
In reply to post #5
Im 2. schritt der musterlösung werden bei der skolomization die foralls vor den exists quantoren entfernt, darf man das deswegen machen weil die exists quantoren im nächsten schritt auch zu voralls umgewandelt werden?
Aaah weiah, da ist was beim umschreiben schiefgelaufen :D Die Quantoren sollten natürlich erst NACH dem negieren rausgeschmissen werden - sie sind aber "richtig" substituiert, weil das nur ein tex-copy-paste und kein rechenfehler war. Man "darf" das also machen, weil ich's beim rechnen erst später gemacht hab und dann hinterher falsch abgetippt :D
Shadow992
Member since Jan 2014
290 posts
In reply to post #5
Quote by Matombo:
äh jah nur anders: https://en.wikipedia.org/wiki/Prenex_normal_form#Implication
das -> wir aufgelöst dann die exists zu forall regel angewand und dann das -> wieder eingefügt oda so

Lös doch die "->" mal in "~ ... v ..." auf und wende die Äquivalenzen weiter oben definiert an.
Anschließend kannst du das wieder in Implikations-Form unwandeln. ;)
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen