Bestand wählen
Merken

05 Semantic Web Technologien - Aussagenlogik und Prädikatenlogik

Zitierlink des Filmsegments
Embed Code

Automatisierte Medienanalyse

Beta
Erkannte Entitäten
Sprachtranskript
dann wollen wir mal begrüßt wieder recht herzlich heute zur glaubt Vorlesung mittlerweile Semantik der Technologie wir
hatten das letzte Mal aufgehört mit den Ontologien also ich hatte erklärt was man darunter steht sowohl auf der einen Seite historisch motiviert aus der Philosophie herausgehalten und auch noch mal kurz unterhalten was bedeutet unter Logik in der Philosophie was in der Informatik der Philosophie des war noch das ist die Lehre vom was das wieder als auch erklären also ist jedoch dass man versucht zu erschließen was bedeutet dass der überhaupt zu sein welche Kategorien des sei es gibt es und er beschreibt man eigentlich genau das und daher hat sich auch die Informatik quasi den Begriff geht aus aus der Philosophie und dort geht es dann wenn was mit anderen Worten beschreiben wollen und Datenmodellierung und die Daten und die wollen dass ist das Wissen der lustig können wir wissen von ihren und was wollte machen wollen heute bei uns aus anschauen wie man solche und nun wirklich auch formal fassen kann damit man dann auch wirklich mit Ontologie haben mechanisch das heißt mit dem Rechner dann weiterarbeiten kann müssen also immer
noch hier im Bereich Nummer 3 Wissensrepräsentation und durch die Sprache müsste man die wird alle 2 und heute geht es
um Aussagenlogik und Prädikatenlogik was größtenteils von einer Wiederholung ist das quasi sagt Schweinsgalopp welche durch diese beiden Themen über die man sich 1. Line aufhalten kann aber das können Sie alles schon aus dem Grundstudium deshalb welche die wichtigsten Aspekte entsprechend wiederholen und der brauchen
diese Logik ganz einfach um was Land zu haben damit bearbeiten können das heißt die Logik zur Formalisierung ontologischer Modell ist heute sieht
folgendermaßen aus was wir alles machen als 1. mal kurze Grundlagen für die natürlich auch wieder das was geschichtliches zu der Logik erzählen was man damit alles machen kann und dann kommt der entscheidende Punkt müssten in einer Art und Weise natürlich auch sagen was bedeutet den jetzt ein was bedeuten die Zeichen der Logik also müssen sei auch in den Semantik Begriff einbringen und ist das schöne mit Hilfe der modelltheoretischen Semantik schöne Sache die Alfred Tarski zwanziger dreißiger Jahren wenig später bei der vierziger Jahren sich ausgedacht hat kann man sehr schön quasi das was man mit der Logik macht die Semantik dort auf der syntaktischen Ebene unterbrechen und das Ganze dann auch mit dem Rechner mechanisch berechnen dass ist für und dazu schauen wir uns dann 2 Verfahren an die wir brauchen um dann mit logischen ausdrücken tatsächlich rechnen zu können dass eines wir müssen alles dann in eine Normalform bringen vielleicht schon mal gehört auch mal kurz wiederholen einmal für aussagenlogische ganz einfach aus der Prädikatenlogik schon etwas schwerer das nächste Mal dann auch noch für die Beschreibungslogiken das wird der ganz neu und wir müssen uns automatisierte Verfahren zum herleiten von Schlussfolgerungen ansehen und dann als 1. die Resolution können wie sollten sie auch schon und das nächste Mal und dazu auch noch das Tableau Verfahren anschauen auch wiederum alles für die Aussagenlogik für die Prädikatenlogik und am Ende für die Beschreibung und abschließen werden heute mit einige Eigenschaften der Aussagenlogik und der Prädikatenlogik 1. Stufe also dann noch mal kurz weiß PL ist natürlich nicht die die Abkürzung für Prädikatenlogik sondern für prognostischen dort und das steht für aussagenlogische dass es der 1. Punkt an dem man meistens verwirrtes und voll SQL ist für Ost oder Loitsche und damit ist die Prädikatenlogik immer gut aber bevor wir direkt 3 gehen die Logik und ich erkläre was man alles toll ist damit machen kann wenn ich sofort natürlich direkt auf den Boden der
Tatsachen zurückführen Logik ist auch nicht der Weisheit letzter Schluss beziehungsweise das endgültige einzige mit überhaupt arbeiten können und auf das uns verlassen können vielleicht kennen einige von ihnen genau diesen haben Kurt Gödels ein bekannter oder freut Einsteins der hat in den dreißiger Jahren sehr schön Arbeit veröffentlicht mit dem man die komplette mathematische Welt aus den Grundfesten quasi vom hat uns gezeigt hatte er das Loch in der Mitte das kann darf man nicht so wir uns das vorstellen dass funktioniert zwar aber über die quasi zum vernünftigen gekommen dass es vernünftiges also das heißt unvollständige axiomatisierbaren axiomatisierbaren wenn wir nicht kriegt aber alles dabei also kurz würde bedeuten oder der bedeutendste Logiker des 20. Jahrhunderts was hat er eigentlich gemacht der hat sich Beschäftigte haben in den zwanziger Jahren mit der so genannten Kontinuums Verbot ist hat das schon mal gehört kund und zu Prothese Kontinuum der hat jemand so richtig man Mathematik studiert im Grundstudium oder so ok man einfach Kontinuum das Kontinuum bezeichnet man normalerweise die Zahlen klar bezahlen natürliche Zahlen 2 unterschiedliche Dinge und er hat sich damit beschäftigt ja wie viel haben wir denn überhaupt auf und hat folgenden Satz quasi aufgestellt und zwar hatte gesagt haben ja jede Menge die Elemente hat als die natürlichen Zahlen die hat mindestens so viele Elemente wie der dass die Kundschaft gut ist also ganz einfach und sagt man mal was es gibt keine überabzählbare Teilmenge der Zahlen die ihrer Mächtigkeit kleiner ist als der Zahlen ist die Folge daraus also Teilmenge der Zahlen ist ebenfalls so groß wie die reellen Zahlen verschroben ist aber letztendlich so der Mathematik der und das Problem war kann man das zeigen kann man das nicht zeigen damit hatte sich irgendwie beschäftigt und mit der Frage ob die Arithmetik also das heißt die Zahlentheorie axiomatisierbaren das so wenn man irgendwas actio thematisiert weil das heißt dass ich kann aber aus einzelnen Aktionen das heißt einfachen Sätzen Gebäude aufbauen Hilfe logische Schlussfolgerung kann ich beispielsweise die Geometrie auf einige wenige Sätze zurückführen das hat schon Priorität versucht beispielsweise die man mit etwas ist gerade was 2 parallelen und so was das man weiteren dabei von Axiomen aufgestellt nicht anders beweisbar waren mit Hilfe dieser Axiome darauf aufbauend konnte man die ganze Geometrie draufsetzen und das hat auch versucht mit der Zahlentheorie zu machen das hatte deshalb gemacht war um 1900 Warum oder Wozu war zum ganz genau zu sagen hatten anderer sehr großer Mathematiker David Hilbert das war der letzte kann man sagen das letzte Universalgenie unter den Mathematikern der sich nur mit allen Teilbereichen der Mathematik beschäftigt hat und publiziert veröffentlicht hat nicht nur sich auf ein spezielles spezialisiert hat der hat auf Mathematikerkongress Kongress 1919 101 seine berühmten insgesamt 23 Probleme vorgestellt von denen erwartet hat man könnte auf diese Probleme quasi die Lösung grade anbrechenden 20. Jahrhundert und dazu hat auch was die Kontinuum Prothese wird und die axiomatisierbaren alte Arithmetik über meine der festen Überzeugung konnte dass mit dieser Axiomatisierung Keith nicht bekommen und so hat das auch irgendwie die gesamte Mathematik der Welt gesehen bis 1931 Kurt Gödel kamen und Kurt Gödel hat dann eine schöne Arbeit veröffentlicht unter dem Titel über formale unentscheidbar setzte der Principia Mathematica dafür sich die Principia Mathematica ist das ist ein Werk in dem man versucht hat oder den Braste auch noch kennen lernen und weiter Kollege von versucht haben die Arithmetik zu Axiomatisierung und hat gezeigt dass sind zu drehen die lassen sich weder beweisen noch widerlegen und das Ganze ist bekannt geworden unter dem Namen Gödelscher Unvollständigkeitssatz das heißt er also gezeigt wenn man ein hinreichend komplexer Systeme widerspruchsfrei genügend reichhaltig damit ich damit halt die Zahlentheorie hier beispielsweise auch ausdrucken kann wenn ich das habe das nicht hat immer wieder Aussagen oder setzte die aus dem System heraus selbst wieder beweisbar sind noch widerlegt was und damit habe ich was quasi Dinge die nicht quasi den kann also kurz vorm davon als ein System das mächtig genug ist nicht in der Lage sich selbst oder seine eigene Konsistenz zu beweisen Widerspruchsfreiheit zu beweisen am damit aber quasi das geschafft was ihr und Unvollständigkeitssatz kennen und eigentlich hätte man danach mit der Mathematik auf können aber wir wissen ja Mathematik des praktischen Leben natürlich auch von Bedeutung damit müssen wir nicht quasi in die innersten Grundfesten ganz am Anfang zurück und wir konnten trotzdem damit arbeiten wenn wir mit annahm aber aufsetzen offenbar nahm die auch nicht beweisen können dass es also gar nicht so schlecht und wenn sie das ganze diese Geschichte um den Gürtel und um die ganzen anderen Mathematiker die wollte noch kurz ansprechen werden inklusive einiger Probleme die bei der Axiomatisierung der Logik aufgetreten sind sich mal unterhaltsamer Form anschauen wollen ist sehr schön komme ich letztes Jahr schien Logik Comics heißt das dort wird die Geschichte von was der diese Konzept der Mathematik geschrieben hat erzählt da kommt dann würde auch vor da kommt mit dem Stollen von und dort solche Mathematiker und Philosophen und Logiker wie das Problem hatten am Ende ihres Lebens oder aufgrund der Suche nach dieser zwischen Wahrheit und wird verrückt geworden zu sein also insbesondere der Gürtel der so 30 Jahre nachdem er seinen Unvollständigkeitssatz bewiesen hat oder gezeigt hat am Princeton kommen werden dabei ums Leben gekommen ist weiß dass einer ist warum es so weit aus dem Grund weil er paranoid war und geglaubt hat man wolle vergiften also die Leute kamen nicht davon überzeugen dass das essen sollte und dementsprechend sollte man vom leider trauriges Ende für so groß und bekannten Mathematiker aber er war nicht der einzige der letztendlich ein bisschen verrückt war da gab es noch mehrere das können Sie schön und komme Buch sich noch gucken
nicht gibt es am besten und durch das können Sie machen war und ist wieder zurück auf die Erde zu unseren
Logik Grundlagen war nicht kennen also Sie sollten das natürlich im Rahmen ihres Bachelor Studiums Grundstudiums schon mal irgendwann behandelt haben Sie können das auch in den dazugehörigen Lehrbüchern ganz bekannt ist der Logik für Informatiker nachlesen ist im Detail quasi noch nochmal nachvollziehen wollen was wir machen ist quasi eine mehr oder weniger informelle Zusammenstellung der wichtigsten Punkte aus diesem gesamten Buch für das normalerweise Ganzes 1. braucht das schaffen hier heute 90 Vorsitzender 80 Minuten der Fakten sondern bisschen arbeitet jetzt noch ein bisschen was zu Geschichte aus vereinbaren Logik
Grundlagen des Sports selber Logos kommt aus dem Griechischen heißt Wort für die Rede und der in unserem Sinne sowie es verstehen wollen verstehen unter der Logik die die Lehre vom formal korrekt und schlussfolgern oder vom formal korrekt und schließen und warum ist es wichtig dass man das formal korrekt war ganz einfach deshalb wollen das automatisieren wollen genauso wie das schon sehr warm Ramon Llull im 14. Jahrhundert vorweggenommen hat wollen quasi eine Maschine bauen eine Rechenmaschine die in der Lage ist quasi am Aussagen zu beweisen also quasi jetzt hier Logik quasi in irgendeiner Art und Weise zu berechnen zu schlussfolgern neues Wissen quasi aus vorhandenen müssten zu erschließen und ich ist das und automatisieren und der hat mir auch schon in der letzten Vorlesung Herrn Leibniz kennengelernt der diesen Gedanken aufgegriffen
hat und entsprechend dann auch geschrieben hat und das so gemacht hat damals im 17. Jahrhundert hat man seine Briefe hier an diesem Philipp Jakob Standard 16 7 80 in Latein schön geschrieben das will ich jetzt nicht vorlesen ich hab natürlich übersetzt steht auf übersetzt der
ich hab ich darüber übersetzt das steht auch im Block hat das mit reingeschrieben also Leibniz hat sehr schön geschrieben alle menschlichen Schlussfolgerungen müssten irgendeinem bezahlen arbeiten Berechnungsarten auf bezahlen arbeitende Rechnungs Satz zurückgeführt werden wie es sie in der Algebra und Kombinatorik mit den Zahlen gibt und sich nicht nur mit einer unzweifelhaften Kunst die menschliche Erfindungsgabe gefördert werden könnte sondern auch viele Streitigkeiten beendet werden könnten das sichere von unsicheren unterschieden und selbst die gerade der Wahrscheinlichkeiten abgeschätzt werden könnten daher bei der der eigene dies gut streiten und zum anderen sagen könnte lasst uns doch nach also sofern wir alle Aussagen gegeneinander vorbringen quasi formalisieren können können wir quasi nachrechnen war ein geeignetes Kalküle haben und können auf Auto mathematische Art und Weise herausfinden werden von diesen Disputanten recht sollte sich das vorgestellt hat der damals hatten auf so gelang diese charakteristischen Zahlen und ähnliche Sachen am erfunden mit denen das machen wollte er nicht ganz bekommen aber mittlerweile schaffen wir das schon ganz gut kommen quasi Leibniz die hier kommen mit den modernen mit dem oder der modernen Logik nachzuvollziehen müssen
natürlich und die Logik anschauen noch mal 2 Sachen vor Augen führen Syntax und Semantik hatten wir schon in der allerersten Stunde bis war hier speziell in der Logik sind bei uns die Syntax natürlich sämtliche Zeichen 1. ohne Bedeutung sondern nur wir haben die Regeln wie zulässige Zeichenfolgen gebildet werden dürfen und müssen noch gar nicht was die Aussagen und die Semantik in der Logik quasi ist zuständig für die Bedeutung der Zeichen und den Regeln der findet man die Bedeutung von komplexen Zeichenfolge Zeichenfolgen aus der Bedeutung von atomaren Zeichen folgen ableiten lässt wenn man sie oder hatten war auch schon mal gesehen als für uns Interpretationen angeguckt am möchte ich aufdringlich quasi atomare Aussagen interpretiere und darauf aufbauend komplexe zusammengesetzt auf Seiten interpretieren kann am Beispiel der Programmiersprache also hier haben Sie für die kleineren 0 bis 4 negatives Guthaben wäre jetzt der Syntax würde interpretieren wollen und der Bedeutung zuweist und konnte das für uns bedeuten die mit Meldungen negatives Guthaben auf sobald der Kontostand die und 0 Euro zu müssen was wir hier machen nur noch ein bisschen fest das was wir jetzt eigentlich genau unter Semantik verstehen und was wir noch nicht wissen es gibt unterschiedliche Arten von sind die einfachste Art des an ist die
sogenannte intendierte Semantik das ist genau das was wir uns quasi vorstellen was es bedeutet also die durch den Benutzer beabsichtigt der Bedeutung bei dem Beispiel das jetzt hier Abend eines Programms das uns die Fakultät ausrechnete und da ist die tendierte Semantik genau auch diese Berechnung der Fakultät für die das sein soll anders formal fassen möchte steht dann da damit die intendierte Semantik schränkt die Menge aller möglichen Modell oder aller möglichen Bedeutung auf die vom menschlichen Benutzer beabsichtigte Bedeutung ein das ist die vom Menschen tendiert zum an mit der kann man auch relativ wenig fest anstellen würde das Amt des auch natürlichsprachlich beschrieben wir brauchen schon so was eine formale Semantik die uns quasi dann hier in einer
formalen Sprache gibt was das Ganze den bedeutet also die formale Semantik werde jetzt die Definition der Fakultät und die formale Semantik hat zum Ziel jetzt die Bedeutung von Zeichenketten in unserem Fall Programmen auszudrücken einer formalen Sprache zu beispielsweise hier mit der Notation wie wir sie aus der Arithmetik so dass sich über das Anwenden von Ableitungsregeln also dass sich daraus was schlussfolgern keine Aussagen über die Zeichenketten beweisen lassen das ist das was man damit machen wolle und damit zum 3. Semantik die für uns zu Moment nicht so wichtig
ist dass es die prozedurale Semantik und das ist das Verhalten des Programms während der Ausführung also eigentlich die Bedeutung eines sprachlichen Ausdrucks bis die Prozedur die internen abläuft wenn dieser Ausdruck fällt prozedurale Semantik ist auch ganz wichtig in der Linguistik in der Psychologie aber für uns jetzt hier weniger von Bedeutung was wir brauchen ist eine formale Semantik und brauchen wie wir quasi von dem was wir haben den sprachlichen Ausdruck auf die formale Semantik nach Art und Weise kommen und da hat uns geholfen der hat hat Alfred Tarski vielleicht hat
irgendjemand zufälligerweise als formale Sprachen gemacht hat in der theoretischen Informatik auch schon mal was von den Notation an das antike gehört der Tarski eingeführt und ich weiß nicht ob das noch unterrichtet wird es jetzt nicht mehr so mild das aber das schöne Sache von uns von machen möchte aber neben der Denotational Semantics hatte die so genannten und theoretische Semantik eingeführt und das ganz besonders wichtig dass wir sogar dass er gesagt hat dass die das versucht die formale oder die Zeichenkette die Art formal zu interpretieren diese Interpretation in Form eines Modells anzugeben einfachste Version dieses Modells für die Aussagenlogik beispielsweise sind zu Preisen von Wahrheitswerten wahr und falsch zu den einzelnen Aussagen über haben und dann kann man die jungen Tumoren also rund oder nicht kann man beschreiben durch Wahrheitswerte darf mit Hilfe der Wahrheitswerte darf kann man dann quasi formal am aussagenlogische Ausdrücke interpretieren und herausfinden ist dieser Komplex Ausdruck jetzt wahr oder falsch nicht Wahrheitswerte Tafeln benutzte das dafür durch das ganze quasi die Aussagenlogik auf so ein ganz einfaches Modell zur also die modelltheoretische Semantik Machthabers geht nimmt die semantische Interpretation künstlich und natürlicher Sprachen dadurch vor dem sie die Bedeutung mit genau definierten Interpretation in einem und gleichsetzt also das was wir alles Interpretation jetzt kennenlernen werden sind feste Modelle den quasi Abbildungsvorschriften gegeben werden wie man Zeichenketten wird in der Logik durch die Syntax vorgegeben haben auf eine Bedeutung das ist genau dieses den was wir dazu braucht das gehe Buchmarkt lebt nicht mehr brauchen sie bedeutende amerikanische aus Polen stammende Mathematiker und Firmen ja der hat sich Grünen auch einen solchen Dingen gearbeitet wurde die so die Grundfesten oder die Grund das grundlegenden Mathematik herausfinden hat schon ein Jahr vorgelegt wurde sowas annähernd ähnliches publiziert die den Unvollständigkeitssatz hat also nicht Gedanken gehabt allerdings kann würde dann mit der vollständigen arbeiten zu 31 und auch noch zuvor bei der quasi selten zu dieser Zeit gearbeitet na
gut Scharons formal an eine Logik ist hier nichts anderes als genau das was würde nämlich eine ganze Menge von Sätzen und verbrauchen Schlussfolgerung Eskalation und muss sich aus den setzen die ich habe was schlussfolgert das heißt ich betrachtet zum eine Teilmenge von diesen setzen dass dieses große und ich betrachte einzelne Sätze die ich aber das ist das kleine und dann kann ich und kann aus einer Teilmenge aller setzte die ich habe dieses klar die hier am Ende dann folgt also ist eine logische Konsequenz von diesem große 4 sind immer für sein ist eine logische Konsequenz von groß oder aus dem Setzen von groß die von einem gleichzeitig einen anderen Buchstaben aber so hat sich das ganze eingebürgert englischen klingt das nicht so schön zweideutig und war sehr schön ist dabei bin ich quasi aus dem Einsatz oder aus der eigenen Teilmenge neben den Einsatz quasi einen andern herleiten kann und umgekehrt diese Herleitung machen kann dann sind beide Sätze logisch äquivalent können es auch schon das ist und viele ist hier ebenfalls äquivalent zu Ziel griechischen Buchstaben und auch für den Lehrer ok also auf diesen Grundsätzen quasi basiert jeder einzelne Logik aussagenlogische genauso wie Prädikatenlogik genauso wie die Beschreibung des Logiken die bei uns anschauen werden schon und jetzt die einzelnen an und gucken wo unterscheiden sie sich denn eigentlich und die geschichtlich betrachtet ist die Aussagenlogik
die ältere der beiden Logiken also da hat man ja schon in der Dora Chrysippos von Soli ab dem 3. Jahrhundert vor Christi Geburt hier eine grammatikalische Logik definiert das komplette Jungautoren Logik mit Konjunktion Negation dann hat die Implikationen hatte Konditional genannt und alternative das war so was wie 6 Uhr und am natürlich aber das Ganze jetzt nicht formal so ausgedrückten sondern dazu das sondern als natürlicher Sprache ausgedrückt was die Arbeiten von den Leuten ja natürlich sehr sehr schwer oder schwierig lesbar macht aber letztendlich dieses schon relativ alte Wissenschaft drum gekümmert und diese Aussagen Logik hat sich dann erst im 19. Jahrhundert wieder Herrenabend Google in allen bekannt aus
der Booleschen Algebra Schaltalgebra George Boole ganz interessant war eigentlich Lehrer und zwar Waldorfschule oder Grundschullehrer Form und hat in seiner Schule auch Schulleiter seiner eigenen Schule also hat auch selber da allein im unterrichtet waren sehr kleines Dorf festgestellt hat nicht viel Geld gehabt musste Schulbücher kaufen für die Kinder und festgestellt dass insbesondere die Mathematik welche alles andere als irgendwie gut waren zu der Zeit in der Schule benutzt hat insbesondere wenn es um die Grundlagen und und die Logik die da wurde da gar nichts gesagt so Rechenarten kennengelernt und ähnliches deshalb hatte angefangen seine eigenen Grundlagen Bücher zu schreiben und hat dann irgendwann hier seine Schriften und 18 40 veröffentlicht die Mathematik wirkt an ist es auf Leute dazu die Grund liegen der Analyst ist der Logik und hat dann die klassische Logik quasi und Aussagenlogik formalisiert und hat dabei auch noch das ist ganz schön Entscheidungsverfahren entwickelt quasi wie man feststellen kann ob eine Formel oder ein Ausdruck wahr oder falsch ist und hat auch hier schon erste Normalform genehmigte disjunktiven Normalform entwickelt allerdings war seine Schreibweise auch noch nicht so ganz über das heute letztendlich mit den Jung von endlichen den verwendeten also Notation man noch ganz anders der nächste Schritt in Richtung vernünftiger Notation
ging aus von Gottlob Frege jener was York gewirkt hat Frege das ist auch einer das werden Sie vielleicht wenn sie das Flugdeck komme nicht mehr angucken feststellen der war auch etwas seltsam als einer der seltsamen Logiker womit der eigentlich ganz normaler Logiker war der hat Form dafür Notation entwickelt hat erwischt Begriffsschrift genannt und schon allein schon der Titel der aber das schön Begriffsschrift hat auch in der Schrift - Titel eine der arithmetischen nachgebildete eine der arithmetischen Sprache nachgebildete Formelsprache des reinen Denkens hat das Land und Wasser damit gemacht hat ist eigentlich Aussagenlogik und auch gleich noch Prädikatenlogik quasi zu axiomatisieren und dafür aber nicht im Kalkül aufzustellen sondern auch und Notation aufzustellen die auch wiederum etwas anders aussieht als das was wir heute verwendeten aber schon relativ nah dran war aber sie sind es doch schon viele bezeichnet das hat sich dann erst später dann geht es nur noch kennen der hat dann die Notation eingeführt so heute ganz wichtig auf dem Weg zur
vollständigen Axiomatisierung ist die Principia Mathematica die von dort 5 was zusammen mit der führten auf weiter geschrieben worden ist sehr diese dickes Buch grundlegendes Buch die beiden an zusammengeschrieben dazu musste das steht auch komme drinnen arbeitet hat derzeit bei was das ging auch nicht so gut mit den beiden zusammen aber sie haben letztendlich gebracht dieses zu schreiben und die Axt also mit axiomatische Fassung der Aussagenlogik damit einzubringen die über dann feststellen mussten oder wie würde dann festgestellt hat bei der manche Sachen unentscheidbar war aber schauen wir mal rein in die Aussagenlogik übers
kennen was haben wir dort wir haben dort die und vor mit denen sich einzelne Aussagen quasi verbinden lassen wir die Negation Konjunktion Disjunktion die Implikationen die Äquivalenz ist ja alles bekannt und wenn wir jetzt Sätze in der Aussagenlogik bilden wollen gibt es natürlich zeugungswillige dafür erstmals in alle atomaren Aussagen setzte die bezeichnet man normalerweise mit Kleinbuchstaben atomaren Aussagen cool ist die usw. und wenn man dann sagen möchte dass ein Einsatz ist dann ist natürlich auch nicht viel die ebenfalls Einsatz und genauso sind dann auch die durch jung Turin verbundenen setzt ebenfalls widersetzte dieser und dann wird noch festgelegt und wie muss ich jetzt komplexe Ausdrücke auflösten dafür gibts Präzedenzfälle also was wird zuerst was bindet stärker was bindet weniger stark unter gezeigt die Regel dass nicht stets vor und und oder steht das steht immer vor der Implikationen und der über das ganz einfaches Beispiel einfache
Sachverhalt oder Aussagen sehen so aus der Mond besteht aus grünem These wäre unsere Aussagen geben es regnet heraus sagte er die Straße der das ist die Aussage und jetzt kann ich daraus 2 komplexe Ausdrücke bauen nicht zum Beispiel wenn es regnet wird die Straße nass das wäre er impliziert oder wenn es regnet und die Straße nicht nass wird dann besteht der Mond aus grünem so das wäre dann wäre und nicht impliziert und können so auch noch Nachricht Nachrichten mit Hilfe von Wahrheitstabellen für diese Oktober ob diese Aussage wahr oder falsch also jetzt endlich ganz einfache Sache Problem dabei ist das hatten auch schon letztes Mal kennengelernt in der Aussagenlogik kann nicht nur über solche atomaren Aussagen treffen die selbst quasi keine innere Struktur haben also die ich sehe nicht an dass da einmal vom Mond und von Grünen Chinesen die Rede des sondern quasi das ist nur ein einfacher Satz unter dem alles Mögliche stehen kann als ich kann keine Aussage über Objekte der Welt und deren Zusammenhänge richtig modellieren insbesondere kann ich keine Aussagen über ganz Mengen von Objekten formulieren dazu brauch ich dann die Prädikatenlogik also nur dann bei der Prädikatenlogik 1. Stufe die dann schon hier von Aristoteles eingeführt worden ist also nicht in der Art und Weise Vorgänger hatten wir oder vor Folge mit dem so genannten Syllogismen also zu solchen Deduktion Street die war das letzte Mal kennengelernt hatten wir hatten diese Schlussfolgerung wegen dieser einfachen sowie kennen kennengelernt das Muster quasi die Aussagen aufgebaut sind damit ich Schlussfolgerungen schlüssig oder korrekt ziehen kann also Sie können das alle Alle Menschen sind sterblich alle Griechen sind Menschen daraus folgt Alec ich sind sterblich und da gibt es einige Muster bei den einmal alle oder einige daneben drinstehen als Quantoren und über quasi die dann entsprechend dem ergibt sich eine ganze Reihe von früher war es halt diese Syllogismen musste man wenn man früher quasi das Studium der 7 Freien Künste betrieben hat auswendig lernen um solche Argumentation zu folgen dann zurückführen zu können auf solche Deduktion Zweck um zu sehen ob man richtig geschlussfolgert hatte war alles sehr schwierig weil alles natürlich in natürlicher Sprache und jetzt nicht irgendwie formal gepackt formal hat das Ganze dann erst wieder Gottlob Frege
entsprechen formalisiert mit seiner Begriffsschrift die war schon hatten und dann so wie wir es heute kennen hat das als das wir zusammen mit
seiner Studenten entwickelt der hat die Syntax so eingeführt wie wir jetzt auch dann kennen werden also die Quantorenlogik der heute üblichen NAT Notation schauen war die Prädikatenlogik 1.
Stufe was kommen neue dazu dass diese Quantoren nämlich Mittel mit denen ich dann die Möglichkeit gegeben bekomme Aussagen über einzelne Dinge innerhalb einer Gruppe von denen zu sagen also das ist der Existenzquantor x existiert irgendetwas innerhalb einer Gruppe von denen oder ich kann Aussagen treffen die für alle Mitglieder einer Truppe Gruppe gelten und das ist der alte Quantor oder Universal und also das ist das für alle und neben den jungen toben hab ich auch noch ein bisschen bereit das Vokabular als bei der Aussagen und nicht auf der einen Seite Variablen die für Konstanten stehen können oder für Wahrheitswerte ich hab Konstanten die stehen für welche den über dich Aussagen machen möchte ich hab Funktionen über konstant über Variablen und ich hab auch noch liegt Relationen und Prädikate war die ich dann hier die unterschiedliche Stelligkeit haben können und über die die mit den nicht haben Formen und andere Sachen dann zusammensetzen kann also das wird immer komplexer das heißt es dann erst mal unten an sich von einem 1. mal so genannte richtige Tagung zu formen das mach ich aus variablen Konstanten Funktion zum wurde sie hier für jetzt hier eine Funktion zum wohl als Funktionen große x wäre jetzt die Variable und das ganze zusammen ist einen Tag genauso wie jetzt zweistellige Funktion die von A und das 2. Argument ist wieder eine Funktion von Y und so weiter also ich kann mir da alle möglichen Sachen ausdenken Hauptsache das ist eine Funktion und keine Relation Relation dazukommen oder jetzt auch hier Kreditkarte in dem Fall dann passt nicht so ausdehnt haben so genannte Atome das ist das was in der 2. 2. Zeile finde also ich setze Atomen noch aus Relation Symbolen zusammen deren Argumente Daniel sind die weiter oben definiert haben und wenn ich dann am Ende auch noch jung und Toren und Formeln alles Mögliche mit dem Spruch Entschuldigung und Quantoren verwendet dann kann ich aus den Atomen komplette Form machen und wie man das macht dafür gibt an entsprechende Syntax die erfüllt werden müssen wenn wir jetzt nicht im Einzelnen durchkauen ich nehme an Sie sind sowieso vertraut mit einfachen aussagenlogischen und prädikatenlogischen ausdrücken wichtig ist dabei immer im Zweifelsfall wenn man nicht weiß ich Reihenfolge abgearbeitet wird Klammern Klammern können Sie auch wenn man nach außen aufgelöst und sollten so gut wie wie alle Variablen die in einer Art und Weise quantifiziert werden das wäre ganz gut um zu sagen ob das jetzt nur für eine oder für alle die Art und Weise die kann ich damit Sachverhalte Formeln Form die den eigentlich relativ einfach Wir müssen nur wissen wie kann ich den quasi aus der natürlichen Sprache dann leiten die entsprechende formale Variante aus der Prädikatenlogik einfaches Beispiel erst mal alle Kinder die meist das heißt also ich spreche über alle x die Variable x benutze ich hier und ich sage wenn ein Kind als wenn x ein Kind ist dann liegt x auf jeden Fall auch Eiscreme und das soll für alle gelten also alle Kinder die ein bisschen komplizierter jetzt über alle x und alle Y sage ich X Vater von Y. ist das ist gleichbedeutend damit das haben x quasi der männliche Elternteil von Y ist also der Vater einer Person ist nicht bekannt hat noch sehr schöner Aussage Es gibt eine oder mehrere als es existiert zumindest eine Vorlesung oder Vorlesung die gleichzeitig auch interessant sollen sich nicht die ausschließen oder andere Sache die Relation ist Nachbar diese Relation ist eine symmetrische Relation das wirklich dadurch aus und den ich sage mal x für alle Y wenn gilt X ist machbar von Y dann gilt auch Y ist Nachbau von X und damit dass das Ganze so galt das Ganze auch noch mal Urlaub weil sie oder Aussagen Zeugen ohne die entsprechende natürlichsprachlichen Darstellung der sind jetzt gefragt waren und man kann sagen was die 1. Zeile hier in natürlicher Sprache als versuchen so es ist doch nicht so schwer es geht um den X ist ist was ich mache das also zur älteren ist dann ist es dann ist gleichzeitig auch ein Mensch und es muss ein Elternteil zu von irgendjemandem also ganz natürlichsprachlicher Ausdrücke muss man natürlich versucht den Satz darzustellen dass man nicht x und y sagt dass da muss man dann ein bisschen dran umfallen das ist dann so passt das ganz allgemein versteht man auch ein bisschen mehrdeutig aber es oft nicht so einfach gut schon zum 2. Mal perfekt der 3. ganz genau und das letzte dürfte wieder ganz einfach sein Mannesmann Onkel oder der ist mein Onkel nicht nur fort genau ganz genau also um Köln sind immer in dem Fall die Brüder meiner Eltern ganz einfach so gut etwas komplizierter wird es dann bei diesem schönen
Beispiel dass wir schon aus dem kleinen Cartoon könnten da ist quasi diese den Geschichte nochmal entsprechend versucht darzustellen die wenn man sie so lesen würde bedeuten würde auch für alle alle gilt also alle Grüne sind schwarz war es außerdem gibt es aber alte Fernsehsendungen die auch Schwarzweiß sind daraus folgt dass einige von eventuelle alte Fernsehsendungen das dann natürlich irgendwo knackt drin es scheint uns erscheint und logischerweise und natürlich auch beweisen können muss die herausfinden wer kann ich die Aussage so stehen lassen wie sie da steht ist sie allgemeingültig also geht sie auf die sie erfüllbar oder kann ich da eventuell einen Widerspruch nachweisen dass sie nicht also wirklich wie ich das mache dazu brauche ich natürlich erstmals die Möglichkeit abzuleiten quasi deren Bedeutung oder deren Semantik nämlich da muss ich jetzt und muss auch
wirklich für genau diese Aussagen modelltheoretische Semantik zusammenbasteln das von uns nächsten Schritt man schon das Ausschau also auch
aussagenlogische einfachster fallen modelltheoretische Semantik das hatten wir schon auf der Folie mit zusammengefasst was ich machen muss ich muss erst sämtliche atomaren Aussagen nach wahr oder falsch ab also hat man Aussagen wie Es regnet wahr falsch berechnet wird oder nicht nach dem Muster einsetzen und muß wahr oder falsch dafür einsetzen sondern jetzt nach vorne habe und ist Interpretation ist von F einfach nichts anderes als die Interpretation einer Formel einen Wahrheitswert mittels dieser Wahrheitstafeln ermittelt werden kann für die dann quasi für jeden jungen CTO steht wie sich die Wahrheit ist einer der Interpretation der ermittelt und da sehen Sie ganz einfach eine einmal p und q die sind einmal erst beide falsch eines davon war und dass beide war und dann steht da was passiert für die nicht was das sie für die Disjunktion oder Hubert als jetzt P und Q was passiert für die Implikationen und für die Äquivalenz also darstellen dann die entsprechenden Wahrheitswerte diese CTO drin die uns als Informatiker natürlich auf jeden Fall geläufig sein sollten die ich nicht noch mal von vorne nach hinten vorlesen auch also das ist genau das man quasi der Aussagenlogik nachweisen kann oder eine modelltheoretische Semantik für die einzelnen und und dann auch für komplexere Aussagen Aufbau der wir brauchen noch ein bisschen mehr und zwar müssen wir
genau wissen wann eine Interpretation ein so genanntes Modell einer Formel ist das ist genau dann wenn ich quasi wenn die Formel die ich aus dieser Interpretation mit der Interpretation bilden kann herleiten kann wenn die war es dann ist die Interpretation ein Modell der Formel das heißt es in dem Fall eine erfüllen der Bestätigung ist das Ganze war und dann gibt es einige Regeln bezüglich der Semantik das heißt wie kann ich jetzt ausgehend von einem atomaren Aussagen auf komplexere Aussagen schließen wenn ich jetzt ein als Modelle quasi von nicht viel betrachte also von einer negierten Form dann ist die kein Modell von vielen also dass ist ein Semantik wirklich auch Interpretation und dann muss ich das Ganze noch entsprechend für alle jungen von durchmaßen machen was bedeutet das für und was bedeutet das für oder was bedeutet das für die Integration was bedeutet das für die Äquivalenz dass sämtliche Regeln womit ich dann die Semantik quasi auf weiter mit den Modellen einer Formel und dann kann ich quasi sagen ob quasi eine Formel allgemeingültig ist oder einer Aussage allgemeingültig ist das heißt dass ist jede mögliche Interpretation erfüllt diese Formel dass es dann auch Tautologien ob sie erfüllbar ist es genau einer erfüllbare Bewegung ob sie oder mindestens eine ob sie widerlegbar ist gibt es mindestens eine nicht erfüllen Bewegung oder ob es unerfüllbar ist das heißt jede Interpretation egal welche haben erfüllt diese Formel nicht also diese Begriffe hatten war oder bei letztendlich alle schon gut das ist noch relativ einfach bei der Aussagen über das verworren und damit auch gar nicht weiter aufhalten sondern wo uns mal anschauen wie sie das Ganze dem dann bei der Prädikatenlogik aus bei der Prädikatenlogik hab ich schon ein bisschen komplizierter Satz an den mit dem ich letztendlich arbeiten kann also als allererstes brauche ich hier einen einen Grund Bereich der irgendwelche Konstanten Elemente enthält die irgendwie in meiner Welt und über die Aussagen machen möchte könnte es habe den oder wie auch immer dann brauch ich Konstantensymbole die werden abgebildet auf Elemente von des dann brauche ich Funktionssymbole das Funktionen über die Elemente auf nach der und dann Relationssymbol auf Relation zur gerne die ich dann habe die wenn irgendwann mal Elemente zu innerhalb eines Grund bereits Relationssymbol mit Argumenten werden dann wahr oder falsch und genau so kann ich dann geben kann die CPU oder Quantoren war das es jetzt ganz nett weil das ist eine komplette informelle Beschreibung der modelltheoretischen Semantik der Prädikatenlogik so einfach machen was uns später nicht mehr also das ist eigentlich auch wesentlich komplizierter Wissmann man weit ist das ganze formal gefasst hat freundlichen auch ersparen braucht mindestens eine Vorlesung Stunde bis man das alles komplett hat wenn wir das für die Beschreibungslogiken anschauen wird das Ganze dann wirklich richtig formal und auch ein bisschen komplizierter basiert aber letztendlich auf genau diesen Dingen hier formal sehen können Sie auch noch mal nachlesen Logik für Informatiker mit dem modelltheoretische Semantik noch mal ganz genau ausgebreitet für uns ist wichtig wir wollen dass die Anwender um herauszufinden wie kann ich den jetzt angesichts meiner genuin Aussage zu
einem Abschluss kommen ist diese Aussage allgemeingültig erfüllbar unerfüllbar oder quasi widerlegbar und da könnt ich jetzt Interpretation angeben sieht folgendermaßen aus dem kann ich Grundbereiche fest mit Elementen a b c usw. Ich brauche erst mal hier keine Konstanten und Funktionssymbole weil ich sehe ich hab oben nur vom Jahr Variablen letztendlich mit drinnen und dann kann man zeigen dass diese Form widerlegbar ist das heißt dass sich nicht allgemeingültig ist das macht man dadurch in die man notfalls durch Versuch und Irrtum eine Billigung versucht herauszufinden eine Interpretation herauszufinden unter der die Formel quasi falsch ist also nicht erfüllbar ist das geht wenn man mit unserer ok und man also diese hier oben für das X für die alle x 14 eine Variable ersetzt man konstante A und sagen dann die Interpretation von Ruin von als also an den Grünen sein dass es war also Schwarzweiß sein dass es auch war dann die andere konstante das soll jetzt unsere Fernsehschau sein und sollen zufälligerweise auch schwarz-weißer sein dass dem Versuch war vor auf der anderen Seite sagen wir jedoch haben als selbst sollte eine haben die Schau also keine Fernsehsendung sein also diese Bewegung soll falsch sein und mit genau dieser Bewegung wenn ich das dann setzt hier die gegebene Formel bekomme ich heraus dass der Wahrheitswert dann falsches als sich die ich hier und Folge aus etwas falsch etwas Wahres das funktioniert in dem Fall dann nicht umgekehrt ich verfolge aus etwas falsch aus das war etwas Falsches weil wir ja Pegu impliziert schwarz-weiß für dieselbe Variable dass ist war dann haben wir hier tierische und bei also gibt in dem Fall dass unter anderem die dafür eingesetzt dass dies Schwarzweiß die ist mir schwarzweiße so dass es auch war deshalb ist quasi das was wurde Implikationen steht der teilbar unterteilt dahinter steht das X 1 wo es aber X als in dem Fall aber keine Tiere wie Chilischoten ist das wäre falsch und damit durchaus etwas war etwas Falsches vor das ist falsche Bewegung in den Fall können sich noch mal etwas genauer ansieht gut also damit kann ich jetzt quasi mit dem Hilfsmittel der Interpretation des ich habe kann ich dann hier auch automatisch feststellen ob solche Aussagen allgemein erfüllbar sind das beste Tautologie sehen ob sie einfach nur erfüllbar sind ob sie wieder durch enthalten oder ob sie als ob sie widerlegbar sind oder Option auf was jetzt so mit dem Vokabular und dem Handwerkszeug was durch das wir brauchen um weiterzumachen paar Sachen brauchen wir noch als es geht
zum logische Schlussfolgerung logische Konsequenz dazu müssen wir von Formen betrachten aus dem was herleiten und jetzt gibt natürlich dafür auf Fachbegriffen von vorne mit bezeichnet als Theorie und dann sagt man eine Interpretation ist ein Modell für eine Theorie die für jede Formel dieser Theorie gilt das kommen meine Interpretation ein Modell für jede einzelne dieser Form ist also ist eigentlich auch ganz so und dann ist eine Form der feinen logische Konsequenz aus der Theorie Themen für jedes Modell von jedes Modell von auch Modell dieser Form ist die sich aus vielerlei Leitung möchte also muss beides war sein und umgekehrt wenn ich aus einer Formel die andere herleiten kann das ganz auf das dann sind beide Formen in dem Fall logisch äquivalent und damit haben wir jetzt alles was wir brauchen um ein Verfahren herzuleiten mit ich die Korrektheit von solchen Aussagen nachweisen kann auf automatische Art und Weise bisschen Spielraum brauchen wir noch müssen und nicht dazu noch logische Äquivalenz
anschauen das kennen Sie auch schon aus der Aussagen und Prädikatenlogik in uns diese einzelnen Gruppen mal angucken da stecken natürlich dann Gesetzmäßigkeiten dahinter schon und zwar war die 1. Gruppe hier links oben an F und die ist äquivalent zu g und f. und das gleiche dann auch noch mit oder was ist davon Gesetzmäßigkeit der ganz einfach ist und die sind austauschbar sind sozusagen kommutativ schon mal gehört der weiß nicht also Kommutativgesetze ist das 1. 2. Gruppe geht die Implikationen die Äquivalenz damit letztendlich nur gezeigt wie kann ich Implikationen und Äquivalenz quasi auflösen und zwar möchte ich dann am Ende irgendwann nur noch von da haben die Konjunktion Disjunktion enthalten das heißt sie wird gezeigt ich aus einer Implikation eine Disjunktion machen sich aus einer Äquivalenz 2 Implikationen macht also das hat keinen besonderen Namen schauen sich dann man 3. Gruppe an auf der linken Seite was könnte das sein schon mal gesehen sieht schön aus also aus Versehen der Tor selbst ändert sich aus und wird oder aus oder wird und und es wird die Delegation nach gezogen das ist was für Gesetzmäßigkeit schon mal gehört die wissen was genau das sind morgen schon habe ich auch noch mal hervorgehoben sie müssen auch wir Augustus De Morgen war schon mal gehört also außer dem Namen dass diese Regeln das entsprechend hat ich schätze nicht und das ist morgen Abend Zeitgenosse auch von George Boole und genauso von Charles an sich mal was von Charles wird stur hatte man was von falsch als mit große Frage wer hat den 1. mechanischen Computer gebaut setzte Fangfrage Natürlichkeit als und hat auch konzipiert also sollten sich mal angucken im 19. Jahrhundert die so genannte am 1. solle das heißt ein mechanischer Computer der in der Lage ist Differentialgleichungen zu lösen und dann die Analytical den also der 1. allgemeinen programmierbare Computer auf mechanischer Basis umgesetzt erst knapp 100 Jahre später ein bisschen auf vereinfachte Art und Weise durch Konrad Zuse und den Freund dieses Charles Albert Bildsprache Rogers das morgen und Schals wird hatte Rogers ist morgen Gebieten seine Nichte und Assistentin der 1. offene ist quasi Mathematik zu unterrichten damit in der Lage ist für seine Knochen buddhistischer Analytical Engine Programme zu schreiben und damit wurde dann daher nach der und der Programmiersprache benannt worden ist quasi 1. Programmiererin der Geschichte sollten sich mal angucken auch schöne Sache dazu gebrauchen komme kann ich noch nicht gesehen zu das oberste lässt und als ok aber noch nicht aber wir haben wir das nächste mit der doppelten Negation doppelten Negation sich auf auch nicht groß zu sagen dann aber ganz unten noch was da wird dann aber es wird da eigentlich gemacht das untere gesetzt dass sich da verbirgt heißen könnte genau das Distributivgesetze Konjunktion und Disjunktion ok schauen wir uns die rechte Spalte an die rechte Spalte der sind junge to mit dabei und da lernen wir was das Quantoren dabei untereinander was passiert war Quantoren und Negation was passiert wenn ich quasi die Negation die quantifiziert Form in hinein holen möchte und da wird aus einem nicht für alle x gilt es wird dann ein es existiert ein X für das nicht direkt also Sie sehen wenn man das reinzieht kehrt sich der Quantum genauso es existiert kein X für das Geld daraus gilt für alle x gilt nicht umgangssprachlich logisch und dann darunter haben wir etwas das hat anscheinend auch etwas damit zu tun dass ich hier Variablen in der Reihenfolge vertauschen keinen werden soll schon mal gesagt ich hat schon mal den was gegeben dass es kommt Aktivität gesetzt das funktioniert ja ganz gut sondern ich mich auf diese Art von Quantoren beschränke was bei unterschiedlichen Quantoren dass das müssen Sie nun herausfinden oder haben Sie mögen herausfinden müssen da sieht das ganz nämlich schon bisschen anders aus unternahm als allerletztes nochmal zu einer Art von bis zu Produktivität für Quantoren kann ich mir jetzt Quantoren zusammengesetzte komplexe vorne auflösen gilt natürlich für jeden Teil das heißt den dementsprechend auch des Distributivgesetze also diese logischen Äquivalenz muss man berücksichtigen und das Problem dass man bekommt dass man sind sehr sehr viele unterschiedliche Aussagen sind logisch äquivalent ist ja das heißt für jede Art von Aussage kann ich potenziell unendlich viele Aussagen schafft die logische Äquivalenz sind also das bedeuten aber komplett anders aussehen und damit habe ich großes Problem da sich nur dadurch lösen kann die ich mir quasi einen
signifikanten Stellvertreter für jede Äquivalenzklassen herauspicke danach ganz bestimmten Regeln zu bilden ist so dass ich dann quasi jede Formel auf einen ganz bestimmten Vertreter einer bestimmten Formen der Äquivalenzklassen abbilden kann und dass die so genannten Normalform und damit kann ich dann sehr leicht Äquivalenz zwischen 2 komplexen ausdrücken nachweisen dass wir diese ganzen Umformungsregeln Weise
gerade eben gesehen haben und das Problem ist über gesagt haben es gibt unendlich groß Äquivalenzklassen Gebrauch davon einen eindeutigen Repräsentanten und Regeln da kommt und dass die genannten Normalform und einfaches Beispiel statt jetzt hier eine mehrfache von zu schreiben ungerade Anzahl schreibt man diese von einem nur einmal weil man dann ständig die sind mit der doppelten Verneinung anwenden kann Ziele bei den Normalform ist es letztendlich quasi eine so genannte Klausel Form zu erzielen werden wir sehen können so wunderbar genau das berechnen was zur Berechnung von Klaus Form des letztendlich nichts anderes als eine sogenannte konjunktiver Normalform das heißt eine Konjunktionen von Disjunktionen da wollen wir das letztlich bringen und wenn wir alle Formen der haben sein wenn eine Konjunktion von Disjunktion bringen oder die damit verbundene aus Form können wir sehr sehr leicht deren Äquivalenz feststellen werden sondern auch gleich bei der Klausel von hier oben rechts das dann nur die Disjunktion und die Konjunktion herausgenommen und sie sehen sich in inneren Klammern das sind eigentlich die Disjunktion die äußere Klammer bildet eine Konjunktion und das macht man das ganze Städtchen kürzer zu schreiben etwas schwierig ist es quasi diese Normalform herzuleiten insbesondere jetzt auch bei der Prädikatenlogik weil sie mir ganz Zwischenschritte brauchen um dann irgendwann in der Klausel Form zum kommenden geht kein Weg dran vorbei das dürfen Sie oder müssen sie in den Übungsaufgaben und wahrscheinlich dann auch in der Klausur durchexerzieren sie müssen quasi wissen wie man aus dem beliebten prädikatenlogischen oder dann bei uns auch Beschreibungslogiken vorne eine Klausel Form herstellt feststellen können die Aussage ist die war ist sie falsch beziehungsweise stimmt Die Schlussfolgerung beweisen wo die Zwischenschritte sehen so aus dass wir als allererstes eine sogenannte Negation Normalform herstellen müssen das heißt sie müssen alle Negation ganz nach hinten ziehen dann müssen bei einem prenex Normalform herstellen können sie wahrscheinlich nicht oder abends schon mal wird in der Logik Vorlesung da müssen alle Quantoren nach vorne dann gehen wir hier eliminieren eine Existenzquantor setzen also dafür dann entweder Konstanten im oder Funktionen einer fest definierten dass es die so genanntes kondensierte prenex Normalform benannt nach Torvalds Call kantig vor der Logik auch noch nicht es auch Mathematiker das eingeführt hat und dann am Ende kann ich daraus dann mit konjunktiver Normalform als mit Tausend Form als müssen uns mal anschauen wie das funktioniert am Beispiel beziehungsweise mit dem einzelnen damit das nachvollziehen können also
von waren mit den einfachsten der so genannten Negation Normalform dafür müssen wir solche Äquivalenz Regeln müsse schon kennen gelernt haben einen wenn mit dem Ziel das sollen als erstes mal einer Formel keine Implikationen keine Äquivalenz der stehen wir wollen ja ganz am Ende dann Konjunktive Normalform haben da sind keine Integration Äquivalenz drinnen dafür hat wir kennengelernt die entsprechende Umwandlungen und dann sollen mehrfach Negation klar wegfallen und dann sollen alle Negation Zeichen es geht direkt vor dem Atom also ganz drinnen stehen also dafür kann ich dann hier diese auch Distributiv gesetzt und auch hier mit Quantoren das entsprechend verwendet wird unserem Beispiel mit Guy und versuchen da jetzt die Negation Normalform zu ziehen wenn sich das angucken das ist ja letztendlich eine große Implikation das heißt die 1. 2 Zeilen der 1. Teil der Implikationen die letzte Zeile ist der 2. Teil der Implikationen müssen entfernen und von der 1. Zeile aber auch noch Implikation das heißt die können war einfach auflösen in dem wir beide dann entsprechend in eine Disjunktion übersetzen sie sind jetzt was reingekommen ist die Verneinung Negation Disjunktion ist rot mit dazu bekommen wir haben jetzt als erstes die Implikationen entsprechend entfernt wird müssen kompliziert also die 1. Implikationen daher wird dann letztendlich daraus dass ich schreibt nicht davor und ersetzte quasi und das oder und auch in muss ich dann quasi ein nicht vor dem Ruin schreiben und vor dem Implikationspfeil oder drauf und das kann nicht entsprechend auch noch umschließt Formen nicht die äußere Negation bis ganz nach Ihnen durch das sieht dann folgendermaßen aus der passieren dann einige sehr schöne Sachen also als allererstes wenn das Negation Zeichen der die 1. klammert sie ändert sich quasi die Konjunktion in der 2. Zeile ganz am Anfang haben die wird mit Disjunktion dann steht hier ein nicht für alle x und dann muss ich das nicht für alle x nach denen sie dann wird aus dem für alle x 1 der existiert X und dann ist das nicht vor der 1. Klammer und dazu die ich dann wiederum auch China und dann wird darum aus dem nicht entgegen X und ein und nicht weit X und so weiter so können Sie man nachvollziehen kann man das Ganze dann entsprechend Uniformen und kommen dann zu dieser rot hinterlegt Form also sollten sich zu Hause anschauen die einfachste Variante wirklich jetzt hier Negation Normalform ist noch ganz einfach dann gehen wir hier und stellen die prenex Normalform er das heißt was wir
machen müssen wir haben eine Formel und sie haben sicherlich gesehen als sie angefangen haben sie zu interpretieren und für diese existiert ein X unterschiedliche Konstanten eingesetzt haben dass das es existiert ein X sich nicht auf genau quasi dasselbe Symbol dieselbe konstante bezieht sondern das können wir unterschiedliche sein also gehen weil er um das sie entsprechend unterscheiden zu können geben wir quasi jedem einzelnen Quandt vor eine unterschiedliche Variable und nicht immer die gleiche Variablen das ändert man nichts dran sie sehen als allererstes 1. Zeile bleibt 2. Zeile wird das Y daraus 3. Zeile wird das draus und wenn wir dann das entsprechend zu geschrieben haben können und können sämtliche Quantoren nach vorne sind und dann haben sie es existiert ein X für alle y und das ist sistiert ein selbst nach vorne gezogen und danach kommen sämtliche Formen ohne die Quantoren also nahm so quasi Quantoren und Formen voneinander getrennt und trotzdem noch die eindeutig zuordnen weil wir ja vor der die Variablen umbenannt haben so weit so gut jetzt kommt der Tricks von Ernst Call und zwar müssen wir irgendwie zu sehen was machen wir denn jetzt hier mit Quantoren müssen ja Interpretation und müssen für die Existenz Quantoren irgendwelche Konstanten also Beispiele für das heißt von den 1. Existenzquantor anschauen der ist existiert ein Xtra kann ich beliebige konstante versetzen also zum Beispiel in A oder was auch immer das mach nicht mit der 2. mit der es existiert ein y als existiert ein Z kann ich da auch eine beliebige konstante versetzt oder habe ich da muss ich mir das 1. berücksichtigen dass ich muss natürlich den 1. Existenzquantor nicht berücksichtigen X und der sind 2 unterschiedliche konstant aber wenn ich dass der Reihe nach nachlesen dass ich sage es existiert ein X und dann geht für alle y und für alle y die da gelten existiert dann eine bestimmte Zeit heißt dass dieses Z ist abhängig von diesem Frankfurt davor das heißt der Bereich aus ich Zeit auswählen kann es eingeschränkt wird nicht zu diesem y dazu und das ist auch der 3. März wollen bei auflösen dieser Formen quasi angewandt hat und der hat gesagt alles quasi was vor so alt kann versteht man vor kein erkannt und möchte das oberste Existenzquantor denn ich habe man davon dings nicht steht dann kann ich da einfach aber nur eine Konstante draus macht umgekehrt werden von meinem Existenzquantor einer oder mehrere von diesen Halbkanton stehen kann nicht ohne konstante draus machen wenn ich sage ist aber abhängig von quasi der Variablen die dort von quasi eine quantifiziert wird und dementsprechend wird eine Funktion genau diese Variable mehrere als kann von stehen wird eine Funktion über mehrere Variablen also das ist der Trick von ganz Call hat erklärt sie sehen also was hier
passiert ja wir es existiert X für alle y und das existiert und das wird dann letztendlich folgendermaßen aufgelöst das das 1. das existiert ein Text durch eine Konstante ersetzt wird und bleibt bestehen also der Bergwand vor und dann der 2. Existenzquantor wird dann eine Funktion über die Variable deshalb vor wird in der Regel noch mal einfach gepasst
geschrieben man geht von links nach rechts vor und entfernt die Existenz Quantoren von links nach rechts gibt es keinen alle Quantor links des zu entfernten Existenzquantor wird die Variable einfach durch ein Konstantensymbole setzt umgekehrt gibt es innerhalb von von links das zu entfernen Existenzquantor so wird die entsprechende Variable durch ein neues Funktionssymbole mit Stelligkeit ersetzt dessen Argumente genau die Variablen die alle Quantoren ansehen und dann kommt man zu genau diesem
dieser schönen formlose gerade gesehen haben wir nur noch einen als Quantor haben und das Schöne dabei ist dann wenn der alte Mann vor darstellen das gilt für alle y sagt man normalerweise nur wenn sowieso für alle gilt dann kann nicht für alle auch weglassen das heißt der nächste Schritt macht es gibt nur noch als von
meiner vor als das ist erst mal weg und versuche jetzt ohne diese Quantoren mithilfe semantische Äquivalenzen das ganze die Klausel Form zu bringen müssen eine Konjunktion von Disjunktion dazu benutzt nicht gesehen hat dieses Distributivgesetze und kommen dann irgendwann ohne dass
jetzt nach rechnen zu wollen am von oben unsere relativ kurzen Formel die etwas längere Formeln dann hier schon entsprechend oder als Konjunktiven Normalform und um das ist schön zu lesen ist es nicht möglich schöner zu lösen kann ist der blau unterlegte Klausel
Formschreiben da hab ich mich anstelle der Konjunktion UND Disjunktion Klammern Gebilde mit drinnen und damit kann ich dann weiter rechts und das man auch gleich dass man damit eigentlich ganz gut rechnen kann also nur noch mal zusammenzufassen was war alles hatten wir hatten als allererstes wenn wir das Umformungen wollen die Negation Normalformen Negation zumal Form und die ursprüngliche Form der sind weil das heißt gefunden durch Äquivalenz Transformation das heißt die sind gleich kein Problem dann hatten als nächstes Relax Normalform Daten unterschiedliche Variablen eingeführt und alle nach vorne gezogen ist immer noch eine Weile dann hatten wir den 3. Schritt School visierte Normalform und da also ein bisschen schwierig das ist nicht wirklich Äquivalenz sondern das ist ja nur ein Beispiel eine Konstante die wir wir als Stellvertreter mit eingesetzt haben das heißt der Schritt normal forms kulminiert School immunisiert des Königs Normalform ist nicht ganz äquivalente Bildern sehen dass das nicht weiter schlimm ist aber dann von der Kolonisierten könne Normalform Niklaus Form dass es wieder über also wenn Sie sich mal angucken versetzte
Formeln die Predigt Normalform Hadis kolonisierte prenex Normalform von die und kamen die Klausel Form von hat das kann ich auch nicht mehr sagen nach 2 Glas war dann kann man feststellen quasi äquivalent die aufgrund der Äquivalenz Umformungen genauso ist hat über den kamen auch aufgrund der Äquivalenz Umformungen aber es ganz wichtig ist nicht äquivalent zu kamen allerdings was noch Geld ist mir nicht ganz am Anfang Farbe und 1. unerfüllbar dann ist Kahn die immer noch und unerfüllbar war das ist so genannte wieder oder dass man versucht dann quasi über diese und als dieser erhalten oder Haltung dieses Unerfüllbarkeit Zustandes oder diese Unerfüllbarkeit Eigenschaften versucht man ein Verfahren war sie zu entwickeln und zwar war dass das Resolution Verfahren das aufgrund quasi auf der Suche oder versucht das schließen oder schlussfolgern auf die Suche nach Widersprüchen zurückzuführen also gleich diese Widerspruchsfreiheit oder dieser Erhaltung dieses Widerspruchs ist sehr sehr wichtig nur dann könne man nicht tatsächlich auch automatisch lustvoll das
quasi dieses Call Kolonisierung keine richtige Äquivalenz Transformation ist kann man daran sehen ein Gegenbeispiel 2. Belegungen gefunden wird anhand dieser Skoll Immunisierung die Phase dann zum Widerspruch führt schauen Sie sich die obere Formel mal an wir haben hier es existiert ein X für das gilt von X oder es existiert kein X für das von ist dass es eine Tautologie weil weder der vordere Teil war des ist der hintere Teil war ich kann das Übersetzen dann oder transformieren mit einer Äquivalenz Transformation Migrations Normalform das heißt was ich mache sich Versuch als erstes Mal die Negation vor dem 2. Existenzquantor nach zu ziehen daraus wird das Ganze dann einen Einheit alle Quantor und nicht die ich machen prenex Normalform drauf das heißt aber ich hab da drin stehen es existiert ein X und das gilt für alle y und Geld von von X oder nicht von Y und die ich hier machen das Call Normalform daraus das heißt ich kann und kann den 1. Existenzquantor durch die Konstante H ersetzen und hat dann noch dort stehen für alle y gilt von A oder nicht von Y das ist äquivalent natürlich auch dazu bin ich und das jetzt einfach nur umschreiben mit Transformation und am das für alle y kann ich natürlich vor nicht von Y schreiben und jetzt mit einem Transformation einfach das nicht noch mal raus dann kann ich hier 2 Interpretationen einsetzen das 1. 70 von als ist falsch ein und das 2. setzt sich ebenfalls für eine Konstante einen nicht von Bier und sagt dass es war und dann hab ich hier einen falsch oder nicht war und das ist nach wie vor falsch das heißt damit habe ich eine nicht erfüllen der Belegung gefunden und aber aus dieser Tautologie da am Anfang Widerspruch gemacht und daran sieht man das kann keine Äquivalenz Transformation sein dies Kolonisierung über der mit gemacht haben weil man dann Widersprüche ableiten kann umgekehrt aber kann man zeigen dass quasi man das um unerfüllbar ist ist nach der Kolonisierung das immer noch unerfüllbar beweist bleibe ich auch schuldig können Sie sich auch im Logik für Informatiker Buch dann entsprechend anschauen dann sind auf der sicheren Seite und das funktioniert so wie wie das funktioniert nicht ermittelt automatisch schlussfolgern kann sie werde in der Resolution das
heißt es ein automatisches Verfahren zum schlussfolgern dass es jetzt eigentlich unsere tatsächlich Rechenmaschine für die Logik die bei uns hier Anschauung
erinnern uns noch mal zurück das wollte auch schon hier Leibniz machen und zwar geht es darum dass nach leiten oder was sie herausfinden wollen quasi wann ist eine Formel für einen logische von Konsequenz einer Theorie jedes Modell von The nämlich auch Modelle von für und die Frage ist ja wie kann nicht direkt an mit allen möglichen Interpretation mit von denen ich die ganze Zeit geredet habe arbeiten also was man brauche es letztendlich man muss die logische Konsequenz die mit Hilfe syntaktischer Verfahren abbilden syntaktisch Verfahren Blockade kennengelernt haben und dann gibt es quasi 2 verschiedene Möglichkeiten es gibt so genannte Entscheidungsverfahren die feststellen können ja und es gibt Aufzählung das Verfahren die quasi mir sämtliche Schlussfolgerungen zurückgefahren
Entscheidungsverfahren und damit verbunden die Entscheidbarkeit sind Verfahren nicht immer terminieren und die beides machen können das heißt ich hatten Eingabe hab ich hier ein Modell und möchte daraus kann man das Theorie und ich hab den Satz der nicht aus herleiten möchte und das Entscheidungsverfahren gibt Jan wenn diese Herleitung möglich ist beziehungsweise ein wenn es nicht möglich ist das heißt das terminiert immer dann ist es entscheidbar und gibt ja zurück im Fall der herleitbar kalt und in einen Fall der nicht herleitbar kann und wenn ich das nicht machen kann also wenn das mal nicht klappt dann bleibt immer noch das Aufzeichnungsverfahren diese Entscheidbarkeit damit ich dieselbe Eingabe versuche dann daraus sämtliche setzte herzuleiten nicht leiten kann und daher das terminiert eigentlich nicht notwendigerweise und dementsprechend ist es dann semientscheidbar das heißt wenn ich Einfall Fall hier oben nicht aus kann dann könnt ich zumindest versuchen Aufzeichnungsverfahren Entscheidbarkeit haben wir anzuwenden werden so sehen dass die Aussagenlogik entscheidbares und die Prädikatenlogik letztendlich nur semientscheidbar oder komme zu dem Verfahren logische
Schlussfolgerung wirklich nachzuprüfen automatisch und zwar funktioniert das folgendermaßen wir haben also mit Theorie Menge von Sätzen und wir haben logische Konsequenz der von 0 was wir machen wollen wir wollen wissen ist es nun tatsächlich jetzt logische Konsequenz von dieser Theorie der können wir müssen erst mal alles Umformungen und zwar können wir daraus natürlich vor der Form das der war 0 herleiten können aus dieser Theorie und das ist äquivalent dazu wenn nicht jeder einzelne Formen die ich drin stehen aber Konjunktiv miteinander verknüpft wird dann impliziert dass quasi 11 0 und das ist allgemeingültig also das heißt wenn es 0 eine logische Konsequenz der Theorie 1 bis es ist dann ist dieser Satz 1 und 2 und 3 und impliziert 11 0 allgemeinen das kann ich mir so Form den ich quasi beide Seiten ihre und zwar kann ich sagen warum das Jahr wenn das eine allgemeingültig ist dann ist es Negation unerfüllbar also nicht von 1 und 2 Kinder von denen implizit von 0 bis unerfüllbar des muss ich einfach nur muss dafür quasi nach oder herleiten dass das tatsächlich unerfüllbar ist das kann ich indem ich quasi da einen Widerspruch abgeleitet und um das machen zu können muss sich diese Form diese Implikation diesen wird der Implikationen in eine Klausel Form übersetzt die Klausel Formen sieht so aus 1 und was die Kar und die Klauseln diese die sind dann Disjunktion also wir Konjunktionen von Disjunktionen das ist eine Klausel und daher versuche ich drin Widerspruch zu also Verfahren der Resolution ist klar wir wollen überprüfen ob neben der Schlussfolgerung stimmt und wir machen das ganz einfach dadurch die wir zeigen dass die Negation dieser Schlussfolgerungen widersprüchlich ein Widerspruch enthält also unerfüllbar ist und dazu genutzt sich die Resolutionen und die Resolution Rahmen sorgt dafür dass sich aus solchen Langform immer kürzere Formeln bekommen und irgendwann mal einen Widerspruch daraus herleiten kann sieht folgendermaßen aus müssen sie auch alle schon mal gesehen habe ich hatte 2 am Disjunktion meiner Klausel Form drinnen im Konjunktiv verbunden sind und ich habe in der eigenen Disjunktion eine Variable p drinnen und habe in der anderen eine Variable nicht darin eine von beiden muß wahr sein einen von beiden muß falsch sein entweder die oder nicht wenn der gesamte obere Ausdruck jetzt war es dann muss auch irgendeines der übrigen Liberale die Billionen drin stehen haben war sein weil ansonsten wird wieder der linke oder der rechte Teil oder werden beide Teile entsprechend dann falsch oder der sind dann falsch war ich habe also das heißt wenn ich und nicht einfach rausstreichen muss der Rest war bleiben die sind Konjunktiv miteinander verbunden also umgekehrt wenn diese Konjunktion unerfüllbar sind das heißt alle irgendwie nicht was ich dann muss natürlich auch die ursprüngliche Form der P und nicht mit drinnen war ebenfalls unerfüllbar sein und dementsprechend kann ich und kann und nicht aus Sonderformen ganz einfach aus und jetzt die Unerfüllbarkeit aus sage am zu gefährden oder zu beeinflussen das heißt diese Resolution Schritt sieht einfach so aus einer Klausel haben 2 Klauseln die hier sehr hinter einem und einmal nicht regiert enthalten und kann ich dann rausnehmen und kann diese beiden Klauseln zusammengeführt wird sich also die Klauseln werden sozusagen dass wir und irgendwann bin ich mal in der Lage aus einer ganzen Klauseln wenn ich Glück habe eine Klausel herzuleiten das heißt dann hab ich nur noch und nicht in den beiden Klauseln ich resultiere drin stehen und daraus folgt dann ein Where-Klausel und dem Button Element bezeichnet und da hab ich dann einen Widerspruch gefunden und bin fertig also das Resolution Verfahren in der Aussagenlogik ist ganz einfach und versucht mit einem Widerspruch Ausnahmen Hause abzuleiten dazu nimmt man 2 Klauseln aus er erzeugt aus denen neue Klausel mit Hilfe dieses Resolution Schritt in diese neue Klausel hat man Widerspruch schon gefunden ansonsten man die Klausel führte zur ursprünglichen Klaus hinzu und macht das Ganze noch mal also schön einfach so komplizierter können Sie sich vorstellen wird das Ganze natürlich der Prädikatenlogik weil dort habe aus natürlich auch noch Quantoren stehen und und von aber nicht Klausel stehen aber der Funktionssymbole der Relation zum wurde drin stehen das am wir so war und der Variablen drin stehen das ist ein bisschen komplizierter als in der Prädikatenlogik letztendlich sieht das dann so aus wie haben wir 2 verschiedene Klauseln sie haben Klauseln wie sie Prädikate und von drinnen und auch noch auf entsprechend ablehnt und was sie machen müssen um die überhaupt miteinander vergleichen zu können müssen beispielsweise manchmal Variablen gegenseitig ersetzt gleichnamig machen wenn man das also so bonifizieren damit sie überhaupt in der Lage sind quasi zu einer Resolution durchzuführen die so Bonifikationen zeitlichen von Zuse gleich noch mal anschauen sieht folgendermaßen aus ich habe 2 verschiedene Liberale und ich versuchen Variablensubstitution zu finden und zwar so als ich kann eine Variable ersetzen durch konstant oder durch Funktion ich versuchen Variable so zu substituieren das gilt quasi dass meine beiden mit realen nach der entsprechenden Substitution gleich sind also Äquivalenz und so eine Substitution ist dann wenn man das schafft beide gleich zu machen ein so genannter Unifikator von unserem mit der realen 1 und 2 der Algorithmus dazu sieht auch wieder ganz einfach aus ich hab also die liberale 1 2 und und und gesuchteste Unifikator Sigma von 1 2 und bin jetzt 1 und 2 nur konstant sind da kann ich nicht groß und infizieren weil man nur Variablen ersetzen kann das heißt die sind dann nur ungefähr bonifiziert war einst tatsächlich von Anfang an gleich 2 ist wenn jetzt eigens eine Variable ist der 2 ein beliebiger kann sind die genauen Daten und infiziert war wenn für die Variable 1 der Kern 2 eingesetzt wird und dabei ganz wichtig die Variable selbst nicht in diesem Jahr 2 vorkommen also das darf ich nicht machen ansonsten kann ich die Variable durch alles Mögliche ersetzte komplizierter wird dann wäre L1 und zwar Prädikate oder Funktionen von bestimmten Stelligkeit sind und die sind nur dann und finanzierbar wenn sie tatsächlich beide gleich sind oder wenn jetzt jeweils die einzelnen Komponenten oder Argumente innerhalb des Prädikats innerhalb der Funktion dann auch tatsächlich bonifiziert Weise miteinander dann funktioniert das auch wieder mal so kompliziert und rekursive Geschichte schauen und zur zum bei einfache Beispiele an
also Sie haben ja einmal 1 und 2 einmal haben 1 2 Variablen stehen und dann von einfach zweimal die bekommt man derart ersetzen Sie ganz einfach x durch A und dann sind die beiden Ausdrücke gleich als unifizierte war der 2. Freitag nicht weil da müssen Sie einmal durch Jahr und einmal durch ersetzt schaffen sie nicht also Sie dürfen nur durch eine weil nicht in dem Fall ersetzt also es gibt es hier keinen Sinn machen dass die beiden gleichnamig macht sie wieder anders aus wenn 2 Variablen haben 2 Konstanten müssen Sie die entsprechende ersetzen und machen x durch A Y durch und dann sind sie ebenfalls möglich ist haben wir 2 Variablen und anderen Ausdruck zweimal dieselbe konstante dann können Sie einmal die Variante X mit aber substituieren einmal die Variable y mit hat substituieren an dann ebenfalls identischen Ausdruck damit sie müssen komplizierter am 1. Ausdruck einmal drin stehen eine Funktion der über die Variable x und das 2. ist eine Konstante und dem 2. aus so kann sie einmal eine Funktion über die Konstante c und dann eine Variable Z müsse sich das 1. mal angucken substituieren dürfen wir immer nur Variablen also auch von vorne an die 1. Variable die befinden wächst die können wir mit der Konstanten c. substituieren dann haben sie die 1. beiden Teile gleicht entsteht bei mal von C dort und und den 2. Teil an 2. Variable die substituieren können sehr sehr können wir nicht ersetzen und schon haben wird wiedergebaut genauso funktioniert dann im nächsten unten drunter das damit ein bisschen komplizierter X für das 1. Mal durch die Variable y ersetzt und widersetzen Z durch 11 von Y und damit können wir beide auch gleichnamig machen allerdings bei der letzten Zeile funktioniert es dann wieder nicht können Sie sich dann auch noch mal überlegen warum das nicht das Nummer um zu sehen so funktioniert Unifikation müssen also keine gleichnamig machen das heißt dann für unsere beiden
Klauseln die wir hier haben wir uns das mal genauer an Cook wir wollen als die Rote hier irgendwie in der Resolution berücksichtigt und zwar müssen wir das so machen dass als allererstes die Variable x durch die konstanter aber setzen und dann das wir die Variable wird durch das von Y ersetzen und das machen aber beides mal dann dort stehen am KIT von A und von Y und einmal nicht von P von A und der von Y das kann wegfallen und dann bleiben falls noch die 2 übrigen Teile der Klauseln dar wobei natürlich auch in den übrigen Teilen der Klauseln die Ersetzung gemacht werden müssen also diese Unifikation Schritte das heißt das dass sie hier haben muss natürlich ersetzt werden durch die Konstante aber das Feld das sie haben muss ersetzt werden durch die Funktion von Ihnen dass Sie dann unten und herausgekommen ist der Q von der von AMD Y oder von der von Y sehen dass sich schon bis komplizierter aus als bei der Aussagenlogik ist aber letztendlich am anhauchst Worte lässt sich schön automatisiert machen das ganz
dann auch an einem richtigen Beispiele Beispiel kennen war schon dass es wieder dieses Harry-Potter Beispiel prädikatenlogische Resolutionen der Wissensbasis einmal terminologisch es wissen das und sagt was ist ein Mensch nicht das was schon gesagt dass ein Elternteil besitzt und was ist ein Waisenkind Waisenkind hat auch gesagt ist auf der einen Seite menschlichen auf der einen Seite ist kein Bestandteil der am Leben und wir haben 2 Individuen wir einmal das Waisenkind Reporter das definiert wird und wir haben einmal eine Beziehung endlich Chance bot ist ein Elternteil von Harry Potter und die Frage ist jetzt die wir und stellen können wir aus dieser Wissensbasis schlussfolgern dass Chance fortan nicht mehr am Leben ist das können war und zwar müssen wir folgendes machen müssen und das Wissen und müssen Fragen können wir daraus hier von diesen letzten Tag herum schlussfolgern dass heißt beschreiben ganz einfach am unsere komplette Wissensbasis mit mitunter miteinander verknüpft und unten drunter versuchen wir daraus zu reduzieren das Wort nicht mehr an also ganz einfach das was wir zeigen wollen und einer Schlussfolgerung geschrieben und das ganze muss allgemeingültig sein wenn das allgemeingültig ist am was gezeigt dann tatsächlich ist Sport nicht mehr so um die Resolution des anwenden zu können müssen einfach müssen das ganze umdrehen das heißt wir einem die ganze Aussage drinnen eine Negation sein ganzes unerfüllbar Torte etwas die und dafür keine zeigen um das zu machen müssen wir das Ganze erstmals die Klausel Form bringen dazu habe ich den
Schritt mit dazu Normalform formal weggelassen hat sollte gleich die nächste Normalform das heißt aber sämtliche Quantoren nach vorne gezogen sie sie das sind zwischen ganz an die hier stehen und habe jetzt auch gleich schon den Schritt gemacht und das Ganze die Klausel Form gebracht müssen Sie jetzt nicht nachvollziehen können Sie gerne zu Hause noch nochmal nachvollziehen dass sind die Klauseln die am Ende dabei stehen sie Sie hier ist dann am Ende quasi Disjunktion in allen Konjunktion verbunden machen die und von der dann hab ich das ganze Klammern Darstellung beschreiben zu mischen untereinander zu müssen und sie die einzelnen Klaus heraussuchen die wir reservieren können die 1. Schritte damit wir besser
sehen hab ich zu reservieren Klauseln geschrieben und zwar haben wir einmal jene Klausel der steht nicht auf 5 x 1 und nicht heran auf 1 x 1 und dann noch 3. nicht allein y 1 Nummer 7 da haben wir keine und oft Chance Port daher Reporter gesehen also könnt aufkommt bei vor einmal negiert einmal nicht hier und was wir machen müssen ist ganz einfach müssen von oben aus der Box die Variable x 1 zu 1 ganz einfach und durch unsere vorliegen Konstanten setzten das heißt Kriegseintritt der Report y ein Switch Spot und dann können wir gehen können beide Klauseln soll das heißt beschreiben sie zusammen und setzt dann aber quasi streichen können auf aus und setzen für die Variable natürlich entsprechend die Konstanten ein bekommen als neue abgeleitete aus daraus nicht auf von Harry Potter und nicht allein so haben eine neue Klausel wir sind noch nicht bei der Klausel angelangt das heißt müssen weiter suchen was wir irgendwie alles soll hier nicht die um das ganze schnell zu machen Nummer 8 Nummer 9 schauen wir uns mal der beides mal drinnen Alive Porta hier einmal nicht jetzt müssen wir noch nicht mal was Unifizierung das können wir so wie sie ist und können quasi daraus ableiten die Nummer 10 nicht offen Harry-Potter von jetzt eigentlich schon fertig weil wir sie auch die Klausel Nummer 6 besteht man einmal offen Harry Potter und nicht auf Harry Potter und daraus können wir die Where-Klausel schlussfolgern und entsprechend haben wir einen Widerspruch abgeleitet und durch den Umkehrschluss können wir folgern als negierte und so unsere plädierte Schlussfolgerung quasi ist falsch dass es unsere ursprüngliche Schlussfolgerungen richtig gewesen das heißt der Ort ist nicht mehr wenn sie sollen das vor ziemlich kompliziert und diesen einfachen Sachverhalt herauszufinden 2 auch noch alles ganz einfach aber sie müssen sich vorstellen sie hätten jetzt Hunderte oder gar Tausende von Klauseln und müssten daher darauf gucken und versuchen das herauszufinden oder diese Fakten wir Kopf zusammenzukriegen das ist dann nicht mehr so einfach ist es schön wenn ein Rechner diese Arbeit aber kann und das funktioniert da 60 Jahre Eigenschaften noch zu
Resolutionen dazu die Resolution ist sozusagen Widerlegung sich vollständig also wird eine Resolution auf widersprüchliche Klaus angewandt also wenn tatsächlich von Widerspruch drin ist ein existiert eine endliche Folge von Resolution Schritt mit der Widerspruch entdeckt werden kann das heißt also das Verfahren terminiert dass tolle Sache und die Anzahl der notwendigen beweist würde dazu die kann natürlich sehr groß werden das ist das eigentliche Problem das ist ungefähr Bereich mehrfach exponentielle dann in der Prädikatenlogik und das ist natürlich nicht sehr schnell aber am Ende doch quasi das ist eine schöne Sache Problemen am Ende ist es ist nicht entscheidbar also ist Niklaus nicht widersprüchlich dann wird das Verfahren leider nicht nur wenn das das aus am Anfang tatsächlich Widerspruch enthält dann jetzt auch irgendwann ja aber das ist quasi im Moment erst mal dass wir uns wichtige Verfahren mit denen wir Schlussfolgerung oder die Korrektheit Schlussfolgerungen beweisen können und damit auch weil sie zeigen können wie man neues Wissen aus vorhandenen müssten herleiten kann das nächste Mal dann auch noch das Tableau Verfahren kennen lernen dass das ganze bisschen einfacher mit etwas weniger Schriften und weniger Aufwand auch schaffen kann was sonst ganz am Schluss bevor ich sie nach Hause schicken kann noch mal anschauen müssen das sind
grundlegende Eigenschaften dieser beiden Verwandten Logiken nämlich der Aussagenlogik und der Prädikatenlogik sie können sich jetzt überlegen wer von beiden Aussagen über die Prädikatenlogik dass wenn die Unterschiede noch Versuche mathematisch nahezu und zwar
auf die Prädikatenlogik das monoton das ist mir sehr schöne Eigenschaften nicht wenn ich jetzt hier die und die Wissensbasis vergrößere geben keine Schlussfolgerung verloren auf der anderen Seite bin ich schon wieder geben kann und kann quasi aus einem Teilmenge der vorhandenen Theorien eine Schlussfolgerung ziehen gilt das auch für meine komplette quasi Wissensbasis die ich habe das heißt wenn ich die Wissensbasis vergrößere keine Schlussfolgerung verloren so bleiben erhalten und es reicht wenn ich jetzt hier quasi aus einem großen Teil dieser Sätze die ich habe schon quasi das was ich herleiten möchte herleiten kann ich muss also nicht immer alles anschauen und Hilfe dieser Monotonie kann man dann auch sehr schön auch noch mal etwas effizientere Verfahren für die Resolution auch herleiten das möcht ja also es ist zudem
Kontakt Compaq das heißt für jede Schlussfolgerung aus einer Theorie bindet eine endliche Teilmenge der Theorie dass folgt letztendlich aus der Monotonie und am ja sie ist semientscheidbar die Prädikatenlogik 1. Stufe ist sogar in dem Sinne unentscheidbar aber natürlich semientscheidbar den ich quasi von einer logischen Konsequenz endlich also immer eine logische Konsequenz endlicher Zeit nachweisen kann über den Widerspruch aber umgekehrt das kann ich mich in endlicher Zeit nach wie es ist also das terminiert nicht notwendigerweise etwas besser sieht das ganze Haus mit der Aussagenlogik ist nicht entscheidbar da können Sie den
Begriff der Entscheidbarkeit auch sehr schön wieder unterbrechen was kann ich da was kann ich nicht ich kann dort also alle waren Schlussfolgerung tatsächlich auch in endlicher Zeit und ich kann auch alle falschen Schlüsse in endlicher Zeit ich muss nur lange genug suchen diese Verfahren terminieren das heißt es dort gibt es immer terminieren der automatische Beweise auch wenn sie manchmal etwas lange braucht dazu hat die Aussage nur noch kann sich Eigenschaften über zum Teil noch kennen gelernt haben dass man nicht Schlussfolgerungen aus der Theorie hat es nicht genau hier unten drunter diese Konjunktion die Implikationen das ist eine Tautologie also das Benutzen der bei der Resolution und ich kann Entscheidung darüber ob ein Satz mit Tautologie ist oder nicht ganz einfach über Wahrheitstabellen trifft das werden sie auch noch der Übung sehen dass das ganz einfach funktioniert und einfach dieses überprüfen Wahrheitstabellen ist nichts anderes als dass ich versuche quasi alle möglichen Interpretation die ich habe zu überprüfen und damit dann sollte quasi alles wissen aufgenommen was man normalerweise im gesamten Semester Logik an den sind quasi vermittelt bekommt Aussagenlogik und Prädikatenlogik inklusive
eines automatischen Schlussfolgerung Verfahren das Resolution Beweisverfahrens usw. Was soll es gesehen haben das reicht natürlich jetzt noch nicht irgendwie rund um damit jetzt Ontologien zu beschreiben natürlich können Sie und mit der Prädikatenlogik beschreiben aber dadurch dass das ganze unentscheidbar oder nur semientscheidbar ist ist es würde wenn man tatsächlich beim Lesen das heißt Programme benutzen möchte die Schlussfolgerung treffen und dann wieder auf die wartet und niemals aber recht das heißt es wäre schon schön wenn wird eine Basis die tatsächlich noch entscheidbar ist und dazu müssen wir gehen an einige von den Elementen der Prädikatenlogik und den bisschen abschwächen dass die jungen Touren nicht jung von Quantoren ist also über alle Quantor Existenzquantor abschwächen hatten wir schon mal gesehen ganz kurz das wenn wir dann in den nächsten Vorlesungen die
Beschreibungslogiken die Familie Beschreibungslogiken durch nehmen wenn man quasi einen Blick über den Rand dessen was er bisher keinen also unseren Tellerrand hinaus werfen und
werden uns dann mal ich der Beschreibung der Welt mit Hilfe von Beschreibungslogiken mit und uns auch angucken daraus dann richtige und auch ok als Literatur heute
Abend zu nur Aussagen und Prädikatenlogik und zu Resolution finden Sie auch was Semantik Grundlagen und natürlich wenn sie es genauer nach lesen wollen Logik für Informatiker und gibt noch Dutzende oder Hunderte andere Bücher in denen die Logik auch axiomatisch mit allen beweisen wie sie brauchen aufgebaut wird also wenn sie dann sind die haben wollen können sich das jederzeit anschauen und dann auch noch hier dieses Logik Comics
dass sich gerade durch gegeben habe die Suche nach der Wahrheit dass sie dann die Gesicht Geschichte von was der Wittgenstein würden und einen anderen kommt auf das was wir heute vielen Dank
Ontologie <Wissensverarbeitung>
Rechenbuch
Kategorie <Mathematik>
Informatiker
Wort <Informatik>
Ebene
Formalisierung
Wissensrepräsentation
Punkt
Rechenbuch
Inferenz <Künstliche Intelligenz>
Normalform
Terminologische Logik
Prädikatenlogik
Aussagenlogik
Tarski, Alfred
Mathematische Größe
Inferenz <Künstliche Intelligenz>
Zahlentheorie
Natürliche Zahl
Aussage <Mathematik>
Gödelscher Unvollständigkeitssatz
Arithmetik
Logiker
Priorität <Informatik>
Zahl
Teilmenge
Gödel, Kurt
Hilbert, David
Menge
Reelle Zahl
Mathematiker
Kontinuum
Systems <München>
Axiom
Widerspruchsfreiheit
Geometrie
Rechenmaschine
Informatiker
Aussage <Mathematik>
Arbeit <Physik>
Kombinatorik
Kalkül
Inferenz <Künstliche Intelligenz>
Algebra
Mathematiker
Aussage <Mathematik>
p-Block
Zahl
Programmiersprache
Negative Zahl
Menge
Berechnung
Programm
Aussage <Mathematik>
Komplex <Algebra>
ART-Netz
Formale Semantik
Momentenproblem
Formale Sprache
Prozedur
Programm
Arithmetik
Aussage <Mathematik>
Tarski, Alfred
Ausdruck <Logik>
Formale Semantik
Zeichenkette
Inferenz <Künstliche Intelligenz>
Formale Sprache
Prädikatenlogik
Gödelscher Unvollständigkeitssatz
Aussage <Mathematik>
Logiker
Natürliche Sprache
Komplex <Algebra>
Ausdruck <Logik>
Teilmenge
Datensatz
Informationsmodellierung
Herleitung
Menge
Aussagenlogik
Mathematiker
Version <Informatik>
Zeichenkette
Theoretische Informatik
Disjunktive Normalform
Boole, George
Eigenwert
Normalform
Aussagenlogik
Mathematiker
Aussage <Mathematik>
Logiker
Implikation
Natürliche Sprache
Rechenart
Richtung
Entscheidungsverfahren
Dicke
Kalkül
Begriffsschrift
Aussagenlogik
Prädikatenlogik
Arithmetik
Logiker
Formelsprache
Frege, Gottlob
Zusammenhang <Mathematik>
Inferenz <Künstliche Intelligenz>
Prädikatenlogik
Reihe
Disjunktion <Logik>
Aussage <Mathematik>
Wahrheitstabelle
Quantifizierung
Natürliche Sprache
Frege, Gottlob
Ausdruck <Logik>
Objekt <Kategorie>
Äquivalenz
Aussagenlogik
Implikation
Parametersystem
Begriffsschrift
Binäre Funktion
Quantor
Prädikatenlogik
t-Test
Aussage <Mathematik>
Quantifizierung
Natürliche Sprache
Ausdruck <Logik>
Konstante
Mittelungsverfahren
Prädikat <Logik>
Bildschirmmaske
Variable
Atom <Informatik>
Tor <Netzwerk>
Funktion <Mathematik>
Informatiker
Äquivalenz
Aussagenlogik
Disjunktion <Logik>
Aussage <Mathematik>
Implikation
Komplex <Algebra>
Parametersystem
Algebraisch abgeschlossener Körper
Prädikatenlogik
Aussage <Mathematik>
Quantifizierung
Element <Mathematik>
Konstante
Variable
Informationsmodellierung
Informatiker
Terminologische Logik
Äquivalenz
Anwendungssoftware
Implikation
Funktion <Mathematik>
Programmiersprache
Kommutativgesetz
Inferenz <Künstliche Intelligenz>
Boole, George
Distributivgesetz
Prädikatenlogik
Programm
Disjunktion <Logik>
Aussage <Mathematik>
Programmiererin
Quantifizierung
Variable
Bildschirmmaske
Spielraum <Wahrscheinlichkeitstheorie>
Zuse, Konrad
Äquivalenz
Differentialgleichungssystem
Quantisierung <Physik>
Mathematiker
Implikation
Gebiet <Mathematik>
Schale
Inferenz <Künstliche Intelligenz>
Berechnung
Prädikatenlogik
Disjunktion <Logik>
Quantifizierung
Äquivalenzklasse
Konstante
Bildschirmmaske
Konjunktive Normalform
Terminologische Logik
Normalform
Äquivalenz
Mathematiker
Funktion <Mathematik>
Konstante
Variable
Bildschirmmaske
Konjunktive Normalform
Normalform
Äquivalenz
Reihe
Disjunktion <Logik>
Quantifizierung
Implikation
Hausdorff-Raum
Konstante
Parametersystem
Variable
Quantor
Quantifizierung
Konstante
Variable
Konjunktive Normalform
Normalform
Distributivgesetz
Äquivalenz
Disjunktion <Logik>
Quantifizierung
Termumformung
Äquivalenzklasse
Konstante
Übersetzer <Informatik>
Informatiker
Normalform
Äquivalenz
Quantor
Zustand
Termumformung
Widerspruchsfreiheit
Rechenmaschine
Informationsmodellierung
Herleitung
Inferenz <Künstliche Intelligenz>
Aussagenlogik
Prädikatenlogik
Entscheidbarkeit
Entscheidungsverfahren
Parametersystem
Inferenz <Künstliche Intelligenz>
Prädikatenlogik
Disjunktion <Logik>
Quantifizierung
Termumformung
Hausdorff-Raum
Ausdruck <Logik>
Konstante
Prädikat <Logik>
Variable
Datensatz
Bildschirmmaske
Algorithmus
Menge
Komponente <Software>
Äquivalenz
Aussagenlogik
Kerndarstellung
Substitution
Implikation
Resolution <Logik>
Funktion <Mathematik>
Konstante
Variable
Inferenz <Künstliche Intelligenz>
Prädikatenlogik
Aussagenlogik
Wort <Informatik>
Wissensbasis
Resolution <Logik>
Konstante
Variable
Inferenz <Künstliche Intelligenz>
Rechenbuch
Normalform
Disjunktion <Logik>
Quantifizierung
Switch <Kommunikationstechnik>
Hausdorff-Raum
Inferenz <Künstliche Intelligenz>
Momentenproblem
Aussagenlogik
Prädikatenlogik
Aussage <Mathematik>
Logiker
Hausdorff-Raum
Resolution <Logik>
Teilmenge
Endlichkeit
Inferenz <Künstliche Intelligenz>
Aussagenlogik
Prädikatenlogik
Wissensbasis
COMPAQ
Physikalische Theorie
Logischer Schluss
Ontologie <Wissensverarbeitung>
Inferenz <Künstliche Intelligenz>
Quantor
Programm
Prädikatenlogik
Wahrheitstabelle
Quantifizierung
Element <Mathematik>
Entscheidbarkeit
Aussagenlogik
Abstrakter Automat
TOUR <Programm>
Implikation
Informatiker
Terminologische Logik
Prädikatenlogik
Aussage <Mathematik>

Metadaten

Formale Metadaten

Titel 05 Semantic Web Technologien - Aussagenlogik und Prädikatenlogik
Serientitel Semantic Web Technologien WS 2011/12
Teil 5
Anzahl der Teile 13
Autor Sack, Harald
Lizenz CC-Namensnennung - keine kommerzielle Nutzung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen und nicht-kommerziellen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
DOI 10.5446/14265
Herausgeber Hasso Plattner Institut (HPI)
Erscheinungsjahr 2011
Sprache Deutsch

Inhaltliche Metadaten

Fachgebiet Informatik
Schlagwörter prädikatenlogik
aussagenlogik

Ähnliche Filme

Loading...
Feedback