| 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 |
| |
|
| |
|
| |
|
WeitereDescriptionLogics
