skip to main content

kiesler.at
WeitereDescriptionLogics
Back to Page | Back to History

Difference between revisions

Version 1, 2005-04-02 18:21 Version 2, 2005-04-02 18:38
Lines 33 - 39 Lines 33 - 39
   
+++ complement +++ complement
   
NOT C | DELTA^I \ C^I NOT C | DELTA^I \ C^I
   
   
+++ conjunction (Schnitt) +++ conjunction (Schnitt)
Lines 58 - 62 Lines 58 - 254
++ Komplexität ++ Komplexität
   
die meisten Reasoning-Tasks sind p-space vollständig! die meisten Reasoning-Tasks sind p-space vollständig!
   
   
  * conjunction (intersection of individuals)
  * disjunction (union of individuals)
  * negation (complement of individuals)
   
  --> DeMorgan gilt!
   
  Dualität: minimale Zeichenmenge für ALC?
   
  --> FOR_ALL oder EXISTS genauso OR oder AND aussuchen
   
  ++ Erweiterung
   
  Individuals! (Instanzen)
   
  Zusätzlich zu concept / role --> Klassen
   
  Eher Eselsbrücke.
   
   
  Hierarchien! (Taxonomie)
   
  Kann 1st order Logic nicht.
   
   
  ++ Knowledge Bases
   
  * Deklarativ Abgelegt
  * Theorie/Fallbasiertes Wissen
   
  Hier: SIGMA =
   
  Theoretical vs Assertional.
   
  Terminological Axioms C SUBSUMPTED D, C .= D
   
  Student .= Person AND EXISTS NAME.String AND
  EXISTS ADDRESS.String AND
  EXISTS ENROLLED.Course
   
  C(a)
  Typ - Instanz (Instanz a ist vom Typ C)
   
  (Student OR Professor)(paul)
   
  ++ TBox (für die Spezialisten)
   
  TBox: descriptive Semantics
   
  * cyclic statements? (Versteckte Terminierung notwendig!)
  * meistens problembehaftet
   
  Zyklisch entspricht Rekursiv.
   
   
  TBox: letztlich Konjunktion von Definitionen!
   
  Wann erfüllt ein Element die ABox?
   
  C(a) ist vom Typ C
   
  a^I EXISTS C^I
   
  Interpretation von a vs. Interpretation von C
   
  Wann ist Interpretatoion ein Modell einer ABox?
   
  Interpretation = Modell für Knowledge Base (Wenn jede Assertion von A durch I erfüllt ist)
   
  (I)
   
  ++ Logische Implikation
   
  semantische Ableitungsoperation
   
  SIGMA |= phi
   
  (phi=goal, siehe Prolog-Programmierung)
   
  Folgt aus Knowledgebox Professor John?
   
  SIGMA |= Professor(john)
   
  ABox: TEACHES(john.cs415).Course(CS415).Undergrade(john)
   
  TBox: EXISTS TEACHES.Course SUBSUMTED NOT Undergrad OR Professor
   
  ja, wegen reasoning Sevice/Tasks
   
  * Concept Salistability
  * Subsumption
  * Satisfiability
  * Instance Checking <=> Negation hat kein Modell - Beweis durch Widerspruch
   
  Reduction durch satisfiability
  * Concept Satisfiability <-> x st. SIGMA v { C(x) } has a model
   
  ~ 127x gemacht
   
  ++ Taxonomy
   
  Halbordnungsrelation via Subsumption
   
  19 Reasoning procedures
   
  Tableaux Calcus
   
  => Versuch, Formel durch Negation zu beweisen und jeder Teil kein Modell hat.
   
  ++ Konjunktive und Disjunktive Zerlegung
   
  auf Zyklen Aufpassen!
   
  F v G wird zu
  / \
  F G
   
  und
   
  F ^ G wird zu
  |
  F
  |
  G
   
   
  wenn in so einem Pfad dann zB a auf NICHT a folgt, gilt dieser als Abgeschlossen. Sind alle Pfade abgeschlossen ist die Negation nicht erfüllbar und das Modell somit erfüllbar.
   
  ++ Negationsnormalform
   
  nur "UND" und "ODER", Negationen nur unmittelbar vor Atomen. Doppelte Negationen dürfen gelöscht werden.
   
  Jede Formel der Wissensbasis wird im Constraint übergeführt.
   
  Completition Rules: Deterministisch (und) / Undeterministisch (oder)
   
  ++ First Order Example für Tableaux:
   
  vs.
   
  23: Negationsnormalform
  24: Completition Rules
   
  ++ Die UND Regel
   
  S -> M {x:C, x:D} vS
   
  (S=System)
   
  if 1. x: C |~| D is in S
  2. x: C and x:D are not both in S
   
   
  C |~| D ... Konjunktion im System
   
  ++ The SOME Rule
   
  S -> EXISTS { xRy, y:C } US
   
  if 1. x: EXISTS R.C is in S
  2. y is a new variable
  3. there is no z such that both xRz and z:C are in S
   
  C(X) ^= x:c
   
  EXISTS x C(x)
  -----------
  C(x\y)
   
  EXISTS x C(x)
  ---------
  c(x\y)
   
  Ziel: Terminierung sicherstellen!
   
  28 completition Rules ALC
   
  S=Pfad
   
  Damit lassen sich die Pfade aufzählen
   
  29: Clash: Enthält A und NICHT a, zB x:A && x:NICHT A
   
  ++ 39: Expressivity
   
  Terminiert
  Korrekt
  Vollständig
  ------
  Tableaux