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