2 - Ontologien im Semantic Web [ID:10840]
50 von 370 angezeigt

so ein bisschen angedeutet, schauen wir uns jetzt das Problem der

Unentscheidbarkeit von Logik erster Stufe an.

Und an dieser Stelle ist im Skript so eine kurze Auflistung von den ganzen

relevanten Begriffen und nachdem ich vermute, dass nicht jeder das Wissen

total parat hat, können wir das an der Stelle auch mal machen. Das heißt,

können zunächst mal sagen, wir geben uns irgendein Alphabet von Symbolen vor

und sagen jetzt, ein Problem ist dann eine Teilmenge der endlichen Strings über

diesem Alphabet und ein solches Problem nennen wir rekursiv aufzählbar, wenn

wir einen Algorithmus hinschreiben können, der der Reihe nach alle Elemente

von a auflistet.

Genau, es gibt eine weitere äquivalente Formulierung dafür, das ist die

Halbentscheidbarkeit eines Problems.

Also a ist re und re ist eben genau dieses recursively innumerable, was wir

gerade schon hatten. Genau, dann wenn es halbentscheidbar ist und das wiederum

heißt, dass es einen Algorithmus gibt, der auf den Elementen von a mit der

Antwort ja terminiert und auf den anderen nicht näher spezifiziertes

Verhalten hat.

Genau, dann ein Begriff, der vielleicht nicht ganz so prominent in BFS vorgekommen

ist, wir nennen a corecursiv aufzählbar oder recursively innumerable.

Genau, dann wenn das Komplement rekursiv aufzählbar ist.

Und ferner gilt noch folgendes, das Problem a ist entscheidbar, genau dann

wenn es rekursiv aufzählbar und corecursiv aufzählbar ist.

Entscheidbarkeit definiere ich jetzt nicht noch mal, das ist praktisch genau

das hier bloß, dass eben auf allen nicht Elementen von a der Algorithmus mit

nein terminieren muss.

Genau, ist irgendjemand eine der Definitionen hier oder mehrere der

Definitionen hier unklar? Ja, also das ist genau die Definition von corecursiv

aufzählbar, das heißt wir bilden das Komplement von dem Problem, also alles

was nicht da drin liegt und wenn das rekursiv aufzählbar ist, dann nennen

wir das corecursiv aufzählbar. Genau, ja der Beweis hierfür ist auch relativ

einfach. Weiß jemand spontan wie das ging?

Ja.

Genau, genau, also die Richtung von hier nach hier, wenn wir zwei Algorithmen

haben, einen der a rekursiv aufzählbar macht und einen das corecursiv

aufzählbar macht, können wir die beide parallel laufen lassen und einer von den

beiden terminiert ja dann und dann haben wir einen Algorithmus für a, für die

Entscheidbarkeit von a gefunden.

Genau.

Gut und der nächste Tagesordnungspunkt ist dann eben, dass wir uns jetzt

anschauen, welche von diesen Eigenschaften hier die Logik erster Stufe

hat bzw. nicht hat.

Und nachdem das Kapitel hier Unentscheidbarkeit heißt, werden wir

dann sehen, dass Logik erster Stufe eben nicht entscheidbar ist, aber wir können

uns ja mal anschauen, wie sieht es mit rekursiv aufzählbar und corecursiv

aufzählbar aus.

Okay und zwar sage ich, Gültigkeit für Logik erster Stufe ist eins von beiden,

jemand eine Idee welches?

Also Gültigkeit für First-Order-Logik, ich behaupte, dass es entweder rekursiv

aufzählbar oder corecursiv aufzählbar, nicht beides, weil sonst wäre es ja

entscheidbar und die Idee ist ja, dass wir heute zeigen, dass es unentscheidbar

Teil einer Videoserie :

Zugänglich über

Offener Zugang

Dauer

01:26:36 Min

Aufnahmedatum

2018-04-19

Hochgeladen am

2019-04-29 07:49:02

Sprache

de-DE

  • Algorithmen für Aussagenlogik
  • Tableaukalküle

  • Anfänge der (endlichen) Modelltheorie

  • Modal- und Beschreibungslogiken

  • Ontologieentwurf

 

Lernziele und Kompetenzen:

 

Fachkompetenz Wissen Die Studierenden geben Definitionen der Syntax und Semantik verschiedener WIssensrepräsentationssprachen wieder und legen wesentliche Eigenschaften hinsichtlich Entscheidbarkeit, Komplexität und Ausdrucksstärke dar. Anwenden Die Studierenden wenden Deduktionsalgorithmen auf Beispielformeln an. Sie stellen einfache Ontologien auf und führen anhand der diskutierten Techniken Beweise elementarer logischer Metaeigenschaften. Analysieren Die Studierenden klassifizieren Logiken nach grundlegenden Eigenschaften wie Ausdrucksstärke und Komplexität. Sie wählen für ein gegebenes Anwendungsproblem geeignete Formalismen aus. Lern- bzw. Methodenkompetenz Die Studierenden erarbeiten selbständig formale Beweise. Sozialkompetenz Die Studierenden arbeiten in Kleingruppen erfolgreich zusammen.

 

Literatur:

 

  • M Krötzsch, F Simancik, I Horrocks; A description logic primer, arXiv, 2012
  • F. Baader et al. (ed.): The Description Logic Handbook, Cambridge University Press, 2003

  • M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2004

  • L. Libkin: Elements of Finite Model Theory, Springer, 2004

Einbetten
Wordpress FAU Plugin
iFrame
Teilen