Uns fehlen oder und not. ACC hat das. Teaching-Assistant SUBSUMTED NOT Undergrad AND Professor 2 Axiome: * .= real determination (?) * SUBSUMTED primitive definition mit oder / negation +++ primitive concept A | A^I untermenge_von DELTA^I +++ primitive role R | R^I untermenge_von DELTA^I x DELTA^I +++ top (=true) T | DELTA^I +++ bottom (=false) (umgedrehtes T) | (durchgestrichene 0) +++ complement NOT C | DELTA^I \\ C^I +++ conjunction (Schnitt) C |~| D (nach unten offenes quadrat) | C^I AND D^I +++ disjunction (Vereinigung) C |_| D (nach oben offenes quadrat) | C^I OR D^I +++ universal quant FORALL R, C | { x | FORALL y.R^I(x,y) -> C^I(y) } +++ existent quant EXISTS R, C | { x | EXISTS y.R^I(x,y) AND C^I (y) } ++ Komplexität 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