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 = <TBox, ABox>

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:

<COMPLETED> vs. <CLASH>

23: Negationsnormalform
24: Completition Rules

Die UND Regel

S -> M {x:C, x} vS

(S=System)

if 1. x: C |~| D is in S
2. x: C and x 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)

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

Last modified 2005-04-02 16:38 by rck