Was wird in First Order Logics unterstützt, was in Description Logic nicht unterstützt wird?

9

Beim Lesen von Beschreibungslogiken (DL) ist es sehr üblich zu lesen, dass es ein Fragment von Logiken erster Ordnung (FOL) ist, aber es ist schwer etwas explizit zu lesen, was von DL ausgeschlossen ist, das Teil von FOL ist. was DL (mit all seinen Dialekten ALC, SHOIN etc ...) entscheidbar macht. Oder mit anderen Worten, könnten Sie mir einige Beispiele in FOL geben, die nicht ausdrückbar sind durch DL (und welche sind der Grund für Semi / Non-Decidability in FOL)?

    
user3590127 16.07.2014, 14:32
quelle

2 Antworten

4

Die folgenden Fakten über Beschreibungslogiken stehen in engem Zusammenhang mit Entscheidbarkeit:

  1. (eine Form von) Tree-Model-Eigenschaft - diese Eigenschaft ist wichtig für Tableu-Methoden;
  2. Einbettbarkeit in multimodale Systeme - von denen bekannt ist, dass sie "robust entscheidbar" sind;
  3. Einbettbarkeit in die sogenannten bewachten Fragmente von FOL - siehe unten;
  4. Einbettbarkeit in Zwei-Variablen-FOL-Fragmente - die entscheidbar sind;
  5. Lokalität - siehe unten.

Einige dieser Fakten sind syntaktisch, während andere semantisch sind. Hier sind zwei interessante, entscheidungsbezogene und mehr oder weniger syntaktische Merkmale der Beschreibungslogik:

Lokalität (aus The Description Logic Handbook, 2. Ausgabe, Abschnitt 3.6):

  

Einer der Hauptgründe, warum Erfüllbarkeit und Subsumtion in vielen Beschreibungslogiken entscheidbar sind - obwohl sehr komplex - ist das   Die meisten Konzeptkonstruktoren können nur lokale Eigenschaften ausdrücken   über ein Element <...> Intuitiv bedeutet dies, dass   Eine Einschränkung in Bezug auf x wird nicht "sprechen" über Elemente, die sind   beliebig weit (wr.t. Rollenverbindungen) von x . Dies bedeutet auch, dass    ALC und in vielen Beschreibungslogiken eine Behauptung auf eine Person   kann keine Eigenschaften über eine ganze Struktur angeben, die sie erfüllt.   Jedoch nicht jede Beschreibung Logik entspricht Lokalität.

Bewachtes Fragment (aus The Description Logic Handbook, 2. Ausgabe, Abschnitt 4.2.3)

  

Geschützte Fragmente werden von der Logik erster Ordnung erhalten, indem man den   Verwendung von quantifizierten Variablen nur, wenn diese Variablen von   geeignete Atome, bevor sie im Körper einer Formel verwendet werden.   Genauer gesagt, sind Quantifizierer darauf beschränkt, nur in der Form | zu erscheinen   ∃ y ( P ( x , y ) ∧ Φ ( y ))   oder ∀ y ( P ( x , y ) ⊃ Φ ( y ) )   (Erstes bewachtes Fragment)
  ∃ y ( P ( x , y ) ∧ Φ ( x , < stark> y ))   oder y ( P ( x , y ) ⊃ Φ ( x , y ))   (Bewachtes Fragment)
  für Atome P , Vektoren der Variablen x und y und (erstes) geschütztes Fragment   Formeln Φ mit freien Variablen in y und x (bzw. in y ).

Unter diesen Gesichtspunkten analysieren Sie die Beispiele aus @ JoshuaTaylors Kommentaren:

  • .x. (C (X) ↔ ∃y. (likes (x, y) ∧ ∃z. (likes (y, z) ∧ likes (z, x))))
  • ∀x. (C (x) ↔ .z. (FavoritTeacher (x, z) ∧ firstGradeTeacherOf (x, z)))

Die Gründe, warum DL für die Wissensrepräsentation der FOL vorzuziehen ist, sind nicht nur Entscheidbarkeit oder rechnerische Komplexität. Sehen Sie sich die Folie "FOL as Semantic Web Language" an. in dieser Vortrag .

    
Stanislav Kralin 06.11.2017 22:25
quelle
1

Wie Turing und Church gezeigt haben, ist FOL unentscheidbar, weil es keinen Algorithmus gibt, um zu entscheiden, ob eine FOL-Formel gültig ist. Viele Beschreibungslogiken sind entscheidbare Fragmente der Logik erster Ordnung, einige Beschreibungslogiken haben jedoch mehr Merkmale als FOL, und viele räumliche, zeitliche und unscharfe Beschreibungslogiken sind ebenfalls unentscheidbar.

    
Leslie Sikos 30.10.2017 10:26
quelle