Agfa-gevaert Nv · EURONEXT:AGFB
Agfa-gevaert Nv — Technical Presentation (2002)
44 slides from Agfa-gevaert Nv's technical presentation, 2002
Slide 1: An inference program for RDF
An inference program for RDF Master thesis by G.Naudts Open University of the Netherlands Agfa
Slide 2: Standards
Standards Trust Proof Logics Ontology Vocabulary RDF +RDFSchema xML + NameSpaces+ x*MLSchema UNICODE + URI
Slide 3: Case study
Case study Antwerpen -> Train -> Brussel Brussel -> Airplane -> Nice Nice —-> Train -> St. Tropez Today Travel agent Customer Rail Belgium Airport Brussels Rail France Restrictions client * price *time Computer Semantic Web
Slide 4: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 5: RDF / DEMO
RDF / DEMO • Database: Regels: child(X, Y), child(Y, Z) :> grandparent(Z, X). grandparent(Z, X), gender(Z, female) :> grandmother(Z, X). Feiten: child(christine, elza). child(wim, christine). gender(elza, female). • Query: grandmother(Z, X).
Slide 6: WWW aspects
WWW aspects • subqueries • closed / open world • verifiability / trust -> origin • inconsistencies
Slide 7: Implementation
Logic reasoning rules (metarules) Concrete RDF syntax facts and rules Concrete RDF syntax ad Implementation Query Concrete RDF syntax Inference engine kernel Abstract RDF subquery syntax Solutions + proofs Concrete RDF syntax solution Other servers
Slide 8: Inference engine for RDF
Inference engine for RDF • Two versions: 1) Classic structure, well tested 2) Better adapted to the semantic web
Slide 9: Search Tree / DEMO
Search Tree / DEMO child Y). child(Y. Z) :> andparent(Z. X)- grandparent(Z. X). gender(Z. female) :> grandmother(Z. X)-. child(christine. elza). child(wim. christine). gender(elza. female). grandmother(Z, X) gender(Z, female) grandparent(Z, X) child(christine. elza) child(wim. christine) gender(elza
Slide 10: Finite State Machine
Finite State Machine solution backtrack execute builtin solve Ni choose < unification failure end of inferencing
Slide 11: Open World Consequences
Open World Consequences • An open set has no borders • An (open?) set has no complement • An element belongs to set A or set B or not known (no law of excluded middle) • There is no universal quantifier for open sets
Slide 12: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 13: Graph syntax of RDF
Graph syntax of RDF groter groter groter
Slide 14: Graph theory
Graph theory Lemmas Resolution Lemma Closure Lemma Essential points Final Path Lemma Looping Lemma | Looping Lemma Il 1) Proof of soundness Infinite Lemma Duplication.Lemma 2) Proof of completeness Failure Lemma Substitution Lemma | . Substitution Lemma Il 3) Proof of solution Solution Lemma Il Solu
Slide 15: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 16: Logic
Logic • Constructive logic cfr. Escher - architect • Each triple in a proof must exist • Verifiability
Slide 17: Slide 17
Slide 18: IT X cl
IT X cl ¢ Aq =i i 9TXZI SUIAl| 9X OT ar wound 71X2] Suluip mate axe ayjauip mip SAYS I¢ X 12 eseies
Slide 19: [VAR gene tate a]
[VAR gene tate a] ‘ 4 bt it yi yal = aT arid ore
Slide 20: RDF Graph
RDF Graph • URI:http://www.daml.org/2001/01/gedcom/ gedcom# • gd:sun(def:Frank,def:Christine).
Slide 21: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 22: Optimization / DEMO
Optimization / DEMO • Question: grandmother(Z, X) • Solution: fact -> rule -> …. -> rule -> solution = grandmother(elza,wim) • Specific rule: t1, t2, t3, .., tn --> grandmother(Z,X) • child(X,Y), child(Y,Z), gender(Z, female):> grandmother(Z,X). • Other
Slide 23: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 24: Inconsistencies
Inconsistencies • Importance of selected logic • No Ex Contradictione Quodlibet • Trust system • Wait and see
Slide 25: Research questions
Research questions 1) Haskell spec of RDF inference program 2) Soundness and completeness 3) What logics? 4) optimization 5) inconsistency
Slide 26: Case study
Case study Antwerpen -> Train -> Brussel Brussel -> Airplane -> Nice Nice —-> Train -> St. Tropez Today Travel agent Customer Rail Belgium Airport Brussels Rail France Restrictions client * price *time Computer Semantic Web
Slide 27: Slide 27
Slide 28: Questions?
Questions?
Slide 29: DEMO
DEMO 1 start Enter command (? for help): ? h : help ? : help q : exit s : perform a single inference step g : go; stop working interactively m : menu e : execute menu item qe : enter a query p : print the graphs
Slide 30: DEMO
DEMO 2 m&&&& You entered:m&&&&& Please, try again. m Type the command e.g. "e pro11." pro11 authentication example pro21 flight simulation pro31 subClassOf example pro41 demo example pro51 gedcom Enter "e item".
Slide 31: DEMO
DEMO 3 Enter "e item". e pro41 RDFProlog version 2.0 Reading files ... Enter command (? for help): s step: goal: grandmother(_1?Z,_1?X)./10 goallist: grandmother(_1?Z,_1?X)./10 substitution: [] history:
Slide 32: DEMO
DEMO 4 s step: goal: grandparent(1$_$_2?Z,1$_$_2?X)./2 goallist: grandparent(1$_$_2?Z,1$_$_2?X)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)] history: (grandparent(1$_$_2?Z,1$_$_2?X),gender(1$_$_2?Z,female) :> grandmother(1$_$_2?Z,1$_$_2?X)./2,grandmother(_1?Z,_1?X)./1
Slide 33: DEMO
DEMO 5 s step: goal: child(2$_$_1?X,2$_$_1?Y)./2 goallist: child(2$_$_1?X,2$_$_1?Y)./2 child(2$_$_1?Y,2$_$_1?Z)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)] history: (child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z) :> grandparen
Slide 34: DEMO
DEMO 6 s step: goal: /0 goallist: /0 child(2$_$_1?Y,2$_$_1?Z)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,christine)(2 $_$_1?Y,elza)] history: (child(christine,elza)./2,child(2$_$_1?X,2$_$_1?Y)./2) (child(2$_$_1?X,2$_$_1?
Slide 35: DEMO
DEMO 7 s step: goal: child(2$_$_1?Y,2$_$_1?Z)./2 goallist: child(2$_$_1?Y,2$_$_1?Z)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,christine)(2 $_$_1?Y,elza)] history: (child(christine,elza)./2,child(2$_$_1?X,2$_$_1?Y)./2) (
Slide 36: DEMO
DEMO 8 s **** No unification; path aborted. **** s **** Backtrack done. **** s
Slide 37: DEMO
DEMO 9 s step: goal: /0 goallist: /0 child(2$_$_1?Y,2$_$_1?Z)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)] history: (child(wim,christine)./2,child(2$_$_1?X,2$_$_1?Y)./2) (child(2$_$_1?X,2$_$_1?Y)
Slide 38: DEMO
DEMO 10 s step: goal: child(2$_$_1?Y,2$_$_1?Z)./2 goallist: child(2$_$_1?Y,2$_$_1?Z)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)] history: (child(wim,christine)./2,child(2$_$_1?X,2$_$_1?Y)./2) (c
Slide 39: DEMO
DEMO 11 s step: goal: /0 goallist: /0 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)(2$_$_1?Z,elza)] history: (child(christine,elza)./2,child(christine,2$_$_1?Z)./2) (child(wim,christine)./2,child(2$_$
Slide 40: DEMO
DEMO 12 s step: goal: gender(1$_$_2?Z,female)./2 goallist: gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)(2$_$_1?Z,elza)] history: (child(christine,elza)./2,child(christine,2$_$_1?Z)./2) (child(wim,chr
Slide 41: DEMO
DEMO 13 s step: goal: /0 goallist: /0 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)(2$_$_1?Z,elza)] history: (gender(elza,female)./2,gender(elza,female)./2) (child(christine,elza)./2,child(christine,2$_$_1?Z)./2) (child(wim,chr
Slide 42: DEMO
DEMO 14 solution: Solution: Substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)(1$_$_2?Z,2$_$_1?Z)(1$_$_2?X,2$_$_1?X)(2$_$_1?X,wim)(2$_$_ 1?Y,christine)(2$_$_1?Z,elza)] Proof: (gender(elza,female)./2,gender(elza,female)./2) (child(christine,elza)./2,child(christine,elza)./2) (child(wim,christine)./2,child
Slide 43: Variable numbering
Variable numbering 1 Enter "e item". e pro41 RDFProlog version 2.0 Reading files ... Enter command (? for help): s step: goal: grandmother(_1?Z,_1?X)./10 goallist: grandmother(_1?Z,_1?X)./10 substitution: [] history:
Slide 44: Variable numbering
Variable numbering 2 s step: goal: grandparent(1$_$_2?Z,1$_$_2?X)./2 goallist: grandparent(1$_$_2?Z,1$_$_2?X)./2 gender(1$_$_2?Z,female)./2 substitution: [(_1?Z,1$_$_2?Z)(_1?X,1$_$_2?X)] history: (grandparent(1$_$_2?Z,1$_$_2?X),gender(1$_$_2?Z,female) :> grandmother(1$_$_2?Z,1$_$_2?X)./2,grandmother