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