|
|
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
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). |
|
|
|
|
|
|
|
|
|
|
subqueries |
|
closed / open world |
|
verifiability / trust -> origin |
|
inconsistencies |
|
|
|
|
|
|
|
Two versions: |
|
Classic structure, well tested |
|
Better adapted to the semantic web |
|
|
|
|
|
|
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 |
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
Constructive logic |
|
cfr.
Escher - architect |
|
Each triple in a proof must exist |
|
Verifiability |
|
|
|
|
|
|
|
URI:http://www.daml.org/2001/01/gedcom/gedcom# |
|
gd:sun(def:Frank,def:Christine). |
|
|
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
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 |
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
Importance of selected logic |
|
No Ex Contradictione Quodlibet |
|
Trust system |
|
Wait and see |
|
|
|
|
1) Haskell spec of RDF inference program |
|
2) Soundness and completeness |
|
3) What logics? |
|
4) optimization |
|
5) inconsistency |
|
|
|
|
|
|
|
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 |
|
|
|
|
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". |
|
|
|
|
|
|
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: |
|
|
|
|
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)./10) |
|
|
|
|
|
|
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)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
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?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./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,christine)(2$_$_1?Y,elza)] |
|
|
|
history: |
|
(child(christine,elza)./2,child(2$_$_1?X,2$_$_1?Y)./2) |
|
(child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
|
|
s |
|
|
|
**** No unification; path aborted. **** |
|
|
|
s |
|
|
|
**** Backtrack done. **** |
|
|
|
s |
|
|
|
|
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),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./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) |
|
(child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
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$_$_1?X,2$_$_1?Y)./2) |
|
(child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
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,christine)./2,child(2$_$_1?X,2$_$_1?Y)./2) |
|
(child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
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,christine)./2,child(2$_$_1?X,2$_$_1?Y)./2) |
|
(child(2$_$_1?X,2$_$_1?Y),child(2$_$_1?Y,2$_$_1?Z)
:> grandparent(2$_$_1?Z,2$_$_1?X)./2,grandparent(1$_$_2?Z,1$_$_2?X)./2) |
|
(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)./10) |
|
|
|
|
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(wim,christine)./2) |
|
(child(wim,christine),child(christine,elza)
:> grandparent(elza,wim)./2,grandparent(elza,wim)./2) |
|
(grandparent(elza,wim),gender(elza,female) :>
grandmother(elza,wim)./2,grandmother(elza,wim)./10) |
|
|
|
|
|
General rule: |
|
"gender(X2,female),child(X1,X2),child(X3,X1) :>
grandmother(X2,X3)." |
|
|
|
|
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: |
|
|
|
|
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)./10) |
|
|
|