diff --git a/RELEASE b/RELEASE index 43e0c961f..5d1387609 100644 --- a/RELEASE +++ b/RELEASE @@ -1,5 +1,6 @@ EYE release +v10.0.0 (2024-03-28) supporting RDF Surfaces, RDF N-Quads and RDF TriG with global scope for blank nodes v9.11.4 (2024-03-04) adding log:query built-in and tested with (un)named graphs v9.11.3 (2024-03-03) lingua is now branch https://github.com/eyereasoner/eye/tree/lingua v9.11.1 (2024-03-03) running lingua with --trig to load TriG data diff --git a/VERSION b/VERSION index c6452b21b..a13e7b9c8 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -9.11.4 +10.0.0 diff --git a/eye.pl b/eye.pl index b67e4a5a3..102ae6fc4 100644 --- a/eye.pl +++ b/eye.pl @@ -21,7 +21,7 @@ :- use_module(library(pcre)). :- catch(use_module(library(http/http_open)), _, true). -version_info('EYE v9.11.4 (2024-03-04)'). +version_info('EYE v10.0.0 (2024-03-28)'). license_info('MIT License @@ -69,7 +69,6 @@ --no-numerals no numerals in the output --no-qnames no qnames in the output --no-qvars no qvars in the output - --no-bnode-relabeling no relabeling of blank nodes in triple or graph terms --no-ucall no extended unifier for forward rules --nope no proof explanation --output write reasoner output to @@ -184,13 +183,6 @@ :- dynamic(''/2). :- dynamic(''/2). :- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). -:- dynamic(''/2). :- dynamic(''/2). :- dynamic(''/2). :- dynamic(''/2). @@ -436,6 +428,170 @@ fail ; true ), + % simplify negative surface + assertz(implies(( + ''(V, G), + getlist(V, Vl), + is_list(Vl), + is_graph(G), + conj_list(G, L), + list_to_set(L, B), + select(''(Z, H), B, K), + getlist(Z, Zl), + is_list(Zl), + is_graph(H), + conj_list(H, M), + list_to_set(M, T), + select(''(W, O), T, N), + getlist(W, Wl), + is_list(Wl), + is_graph(O), + ( conj_list(O, D), + append(K, D, E), + conj_list(C, E) + ; length(K, I), + I > 1, + conj_list(F, N), + conj_list(C, [''([], F)|K]) + ), + findvars(H, R, beta), + intersection(Zl, R, X), + findvars(O, S, beta), + intersection(Wl, S, Y), + append([Vl, X, Y], U) + ), ''(U, C), '<>')), + % resolve negative surfaces + assertz(implies(( + ''(V, G), + getlist(V, Vl), + is_list(Vl), + is_graph(G), + conj_list(G, L), + list_to_set(L, B), + findall(1, + ( member(''(_, _), B) + ), + O + ), + length(O, E), + length(B, D), + memberchk(E, [0, 2, D]), + ''(W, F), + getlist(W, Wl), + is_list(Wl), + is_graph(F), + conj_list(F, K), + list_to_set(K, N), + length(N, 2), + makevars(N, J, beta(Wl)), + select(''(U, C), J, [P]), + getlist(U, Ul), + is_list(Ul), + is_graph(C), + ( select(''(Z, Q), B, A), + M = [''(Ul, C)|A], + conj_list(Q, R), + memberchk(P, R) + ; select(Q, B, A), + M = [P|A], + conj_list(C, R), + memberchk(Q, R) + ), + list_to_set(M, T), + conj_list(H, T), + ground(''(Vl, H)) + ), ''(Vl, H), '<>')), + % convert negative surfaces to forward rules + assertz(implies(( + ''(V, G), + getlist(V, Vl), + is_list(Vl), + is_graph(G), + conj_list(G, L), + list_to_set(L, B), + select(''(_, H), B, K), + conj_list(R, K), + makevars([R, H], [Q, S], beta(Vl)), + findvars(S, W, beta), + makevars(S, I, beta(W)) + ), ''(Q, I), '<>')), + % convert negative surfaces to forward contrapositive rules + assertz(implies(( + ''(V, G), + getlist(V, Vl), + is_list(Vl), + is_graph(G), + conj_list(G, L), + list_to_set(L, B), + \+member(exopred(_, _, _), B), + ( length(B, O), + O =< 2 + -> select(R, B, J), + J \= [] + ; B = [R|J] + ), + conj_list(T, J), + findvars(R, N, beta), + findall(A, + ( member(A, Vl), + \+member(A, N) + ), + Z + ), + E = ''(Z, T), + makevars([R, E], [Q, S], beta(Vl)), + findvars(S, W, beta), + makevars(S, I, beta(W)) + ), ''(Q, I), '<>')), + % convert negative surfaces to universal statements + assertz(implies(( + ''(V, G), + getlist(V, Vl), + is_list(Vl), + Vl \= [], + is_graph(G), + conj_list(G, [G]), + ( G = ''(Z, H) + -> true + ; Z = [], + H = ''([], G) + ), + findvars(H, R, beta), + intersection(Z, R, X), + conj_list(H, B), + member(M, B), + findall(''(Vl, W), + ( member(W, X) + ), + Y + ), + conj_list(S, Y), + append(Vl, X, U), + makevars([M, S], [Q, I], beta(U)) + ), ':-'(Q, I), '<>')), + % blow inference fuse + assertz(implies(( + ''(V, G), + call(( + getlist(V, Vl), + is_list(Vl), + is_graph(G), + conj_list(G, L), + makevars(G, H, beta(Vl)), + ( H = ''(_, false), + J = true + ; catch(call(H), _, false), + J = H + ), + ( H = ''(_, C) + -> I = ''(_, C) + ; I = H + ) + )), + J, + ''(_, I) + ), false, '<>')), + % set engine values ( implies(_, Conc, _), ( var(Conc) ; Conc \= answer(_, _, _), @@ -801,11 +957,6 @@ N is random(2^120), nb_setval(random, N), opts(Argus, Args). -opts(['--no-bnode-relabeling'|Argus], Args) :- - !, - retractall(flag('no-bnode-relabeling')), - assertz(flag('no-bnode-relabeling')), - opts(Argus, Args). opts(['--rdf-list-output'|Argus], Args) :- !, retractall(flag('rdf-list-output')), @@ -1005,8 +1156,8 @@ answer('', A, C), '')), assertz(implies(':-'(C, A), answer(':-', C, A), '')), - assertz(implies((quad(triple(P, S, O), G), \+''(P, '')), - answer(quad, triple(P, S, O), G), '')), + assertz(implies((quad(triple(S, P, O), G), \+''(P, '')), + answer(quad, triple(S, P, O), G), '')), ( flag(intermediate, Out) -> portray_clause(Out, implies((exopred(P, S, O), \+''(P, '')), answer(P, S, O), '')), @@ -1014,8 +1165,8 @@ answer('', A, C), '')), portray_clause(Out, implies((':-'(C, A), \+''(A, true)), answer(':-', C, A), '')), - portray_clause(Out, implies((quad(triple(P, S, O), G), \+''(P, '')), - answer(quad, triple(P, S, O), G), '')) + portray_clause(Out, implies((quad(triple(S, P, O), G), \+''(P, '')), + answer(quad, triple(S, P, O), G), '')) ; true ), args(Args). @@ -2401,15 +2552,11 @@ { atom_codes(Lbl, LblCodes), subst([[[0'-], [0'_, 0'M, 0'I, 0'N, 0'U, 0'S, 0'_]], [[0'.], [0'_, 0'D, 0'O, 0'T, 0'_]]], LblCodes, LblTidy), atom_codes(Label, LblTidy), - ( flag('no-bnode-relabeling') - -> D = 0 - ; nb_getval(fdepth, D) - ), - ( evar(Label, S, D) + ( evar(Label, S, 0) -> true ; atom_concat(Label, '_', M), gensym(M, S), - assertz(evar(Label, S, D)) + assertz(evar(Label, S, 0)) ), ( ( nb_getval(entail_mode, false), nb_getval(fdepth, 0) @@ -10707,6 +10854,10 @@ ; A = exopred(_, _, _) ). +is_graph(true). +is_graph(A) :- + is_gl(A). + unify(A, B) :- nonvar(A), A = exopred(P, S, O), @@ -11438,10 +11589,6 @@ !. quant(answer('', _, _), allv) :- !. -quant(_-A, avar) :- - conj_list(A, B), - member(''(_, _), B), - !. quant(_, some). labelvars(A, B, C) :- diff --git a/eye.zip b/eye.zip index 0c4b342ca..b84423f99 100644 Binary files a/eye.zip and b/eye.zip differ diff --git a/reasoning/bi/biA.n3 b/reasoning/bi/biA.n3 index 7307e7701..ffcd3cb4c 100644 --- a/reasoning/bi/biA.n3 +++ b/reasoning/bi/biA.n3 @@ -491,12 +491,12 @@ { { log:semantics { - :a :b _:e_c_14. + :a :b _:e_c_2. }. { - :a :b _:e_c_14. + :a :b _:e_c_2. } log:equalTo { - :a :b _:e_c_14. + :a :b _:e_c_2. }. } => { :loges3 :result true. @@ -662,12 +662,12 @@ { { log:semantics { - :a :b _:e_c_14. + :a :b _:e_c_2. }. { - :a :b _:e_c_14. + :a :b _:e_c_2. } log:includes { - :a :b _:e_c_14. + :a :b _:e_c_2. }. } => { :logis3 :result true. @@ -790,10 +790,10 @@ { { log:semantics { - :a :b _:e_c_14. + :a :b _:e_c_2. }. { - :a :b _:e_c_14. + :a :b _:e_c_2. } log:notIncludes { :a :b :c. }. @@ -804,13 +804,13 @@ { { log:semantics { - :a :b _:e_c_14. + :a :b _:e_c_2. }. log:semantics { :a :b :c. }. { - :a :b _:e_c_14. + :a :b _:e_c_2. } log:notIncludes { :a :b :c. }. diff --git a/reasoning/euq/euqA.n3 b/reasoning/euq/euqA.n3 index a66602e16..98a9660ce 100644 --- a/reasoning/euq/euqA.n3 +++ b/reasoning/euq/euqA.n3 @@ -2,6 +2,122 @@ @prefix var: . :a :valid true. +{ + ?U_0 ?U_1. + "getlist(some0,some2)". + "is_list(some2)". + "is_graph(some1)". + "conj_list(some1,some3)". + "list_to_set(some3,some4)". + "select(''(some5,some6),some4,some7)". + "getlist(some5,some8)". + "is_list(some8)". + "is_graph(some6)". + "conj_list(some6,some9)". + "list_to_set(some9,some10)". + "select(''(some11,some12),some10,some13)". + "getlist(some11,some14)". + "is_list(some14)". + "is_graph(some12)". + "conj_list(some12,some15),append(some7,some15,some16),conj_list(some17,some16);length(some7,some18),some18>1,conj_list(some19,some13),conj_list(some17,[''([],some19)|some7])". + "findvars(some6,some20,beta)". + "intersection(some8,some20,some21)". + "findvars(some12,some22,beta)". + "intersection(some14,some22,some23)". + "append([some2,some21,some23],some24)". +} => { + _:sk_24 _:sk_17. +}. +{ + ?U_25 ?U_26. + "getlist(some25,some27)". + "is_list(some27)". + "is_graph(some26)". + "conj_list(some26,some28)". + "list_to_set(some28,some29)". + "findall(1,member(''(some30,some31),some29),some32)". + "length(some32,some33)". + "length(some29,some34)". + "memberchk(some33,[0,2,some34])". + ?U_35 ?U_36. + "getlist(some35,some37)". + "is_list(some37)". + "is_graph(some36)". + "conj_list(some36,some38)". + "list_to_set(some38,some39)". + "length(some39,2)" . + "makevars(some39,some40,beta(some37))". + "select(''(some41,some42),some40,[some43])". + "getlist(some41,some44)". + "is_list(some44)". + "is_graph(some42)". + "select(''(some45,some46),some29,some47),some48=[''(some44,some42)|some47],conj_list(some46,some49),memberchk(some43,some49);select(some46,some29,some47),some48=[some43|some47],conj_list(some42,some49),memberchk(some46,some49)". + "list_to_set(some48,some50)". + "conj_list(some51,some50)". + "ground(''(some27,some51))". +} => { + _:sk_27 _:sk_51. +}. +{ + ?U_52 ?U_53. + "getlist(some52,some54)". + "is_list(some54)". + "is_graph(some53)". + "conj_list(some53,some55)". + "list_to_set(some55,some56)". + "select(''(some57,some58),some56,some59)". + "conj_list(some60,some59)". + "makevars([some60,some58],[some61,some62],beta(some54))". + "findvars(some62,some63,beta)". + "makevars(some62,some64,beta(some63))". +} => { + _:sk_61 => _:sk_64. +}. +{ + ?U_65 ?U_66. + "getlist(some65,some67)". + "is_list(some67)". + "is_graph(some66)". + "conj_list(some66,some68)". + "list_to_set(some68,some69)". + "\+member(exopred(some70,some71,some72),some69)". + "length(some69,some73),some73=<2->select(some74,some69,some75),some75\=[];some69=[some74|some75]". + "conj_list(some76,some75)". + "findvars(some74,some77,beta)". + "findall(some78,(member(some78,some67),\+member(some78,some77)),some79)". + "some80=''(some79,some76)". + "makevars([some74,some80],[some81,some82],beta(some67))". + "findvars(some82,some83,beta)". + "makevars(some82,some84,beta(some83))". +} => { + _:sk_81 => _:sk_84. +}. +{ + ?U_85 ?U_86. + "getlist(some85,some87)". + "is_list(some87)". + "some87\=[]". + "is_graph(some86)". + "conj_list(some86,[some86])". + "some86=''(some88,some89)->true;some88=[],some89=''([],some86)". + "findvars(some89,some90,beta)". + "intersection(some88,some90,some91)". + "conj_list(some89,some92)". + "member(some93,some92)". + "findall(''(some87,some94),member(some94,some91),some95)". + "conj_list(some96,some95)". + "append(some87,some91,some97)". + "makevars([some93,some96],[some98,some99],beta(some97))". +} => { + _:sk_98 <= _:sk_99. +}. +{ + ?U_100 ?U_101. + "call((getlist(some100,some102),is_list(some102),is_graph(some101),conj_list(some101,some103),makevars(some101,some104,beta(some102)),(some104=''(some105,false),some106=true;catch(call(some104),some107,false),some106=some104),(some104=''(some108,some109)->some110=''(some111,some109);some110=some104)))". + (?U_106 { + ?U_112 ?U_110. + }) true. +} => false. { var:qu_1 :valid true. } => { diff --git a/reasoning/iq/iqA.n3 b/reasoning/iq/iqA.n3 index 3b96ddd4b..618aae284 100644 --- a/reasoning/iq/iqA.n3 +++ b/reasoning/iq/iqA.n3 @@ -1,18 +1,133 @@ @prefix : . -@prefix var: . _:sk_0 :loves _:e_y_1. _:e_x_1 :says { - _:e_x_3 :knows :Albert. + _:e_x_1 :knows :Albert. }. :s :p :o. :s :pp { :s :ppp :ooo. }. { - ?U_1 :knows :Albert. + ?U_1 ?U_2. + "getlist(some1,some3)". + "is_list(some3)". + "is_graph(some2)". + "conj_list(some2,some4)". + "list_to_set(some4,some5)". + "select(''(some6,some7),some5,some8)". + "getlist(some6,some9)". + "is_list(some9)". + "is_graph(some7)". + "conj_list(some7,some10)". + "list_to_set(some10,some11)". + "select(''(some12,some13),some11,some14)". + "getlist(some12,some15)". + "is_list(some15)". + "is_graph(some13)". + "conj_list(some13,some16),append(some8,some16,some17),conj_list(some18,some17);length(some8,some19),some19>1,conj_list(some20,some14),conj_list(some18,[''([],some20)|some8])". + "findvars(some7,some21,beta)". + "intersection(some9,some21,some22)". + "findvars(some13,some23,beta)". + "intersection(some15,some23,some24)". + "append([some3,some22,some24],some25)". } => { - var:x_0 :knows :Kurt. + _:sk_25 _:sk_18. +}. +{ + ?U_26 ?U_27. + "getlist(some26,some28)". + "is_list(some28)". + "is_graph(some27)". + "conj_list(some27,some29)". + "list_to_set(some29,some30)". + "findall(1,member(''(some31,some32),some30),some33)". + "length(some33,some34)". + "length(some30,some35)". + "memberchk(some34,[0,2,some35])". + ?U_36 ?U_37. + "getlist(some36,some38)". + "is_list(some38)". + "is_graph(some37)". + "conj_list(some37,some39)". + "list_to_set(some39,some40)". + "length(some40,2)" . + "makevars(some40,some41,beta(some38))". + "select(''(some42,some43),some41,[some44])". + "getlist(some42,some45)". + "is_list(some45)". + "is_graph(some43)". + "select(''(some46,some47),some30,some48),some49=[''(some45,some43)|some48],conj_list(some47,some50),memberchk(some44,some50);select(some47,some30,some48),some49=[some44|some48],conj_list(some43,some50),memberchk(some47,some50)". + "list_to_set(some49,some51)". + "conj_list(some52,some51)". + "ground(''(some28,some52))". +} => { + _:sk_28 _:sk_52. +}. +{ + ?U_53 ?U_54. + "getlist(some53,some55)". + "is_list(some55)". + "is_graph(some54)". + "conj_list(some54,some56)". + "list_to_set(some56,some57)". + "select(''(some58,some59),some57,some60)". + "conj_list(some61,some60)". + "makevars([some61,some59],[some62,some63],beta(some55))". + "findvars(some63,some64,beta)". + "makevars(some63,some65,beta(some64))". +} => { + _:sk_62 => _:sk_65. +}. +{ + ?U_66 ?U_67. + "getlist(some66,some68)". + "is_list(some68)". + "is_graph(some67)". + "conj_list(some67,some69)". + "list_to_set(some69,some70)". + "\+member(exopred(some71,some72,some73),some70)". + "length(some70,some74),some74=<2->select(some75,some70,some76),some76\=[];some70=[some75|some76]". + "conj_list(some77,some76)". + "findvars(some75,some78,beta)". + "findall(some79,(member(some79,some68),\+member(some79,some78)),some80)". + "some81=''(some80,some77)". + "makevars([some75,some81],[some82,some83],beta(some68))". + "findvars(some83,some84,beta)". + "makevars(some83,some85,beta(some84))". +} => { + _:sk_82 => _:sk_85. +}. +{ + ?U_86 ?U_87. + "getlist(some86,some88)". + "is_list(some88)". + "some88\=[]". + "is_graph(some87)". + "conj_list(some87,[some87])". + "some87=''(some89,some90)->true;some89=[],some90=''([],some87)". + "findvars(some90,some91,beta)". + "intersection(some89,some91,some92)". + "conj_list(some90,some93)". + "member(some94,some93)". + "findall(''(some88,some95),member(some95,some92),some96)". + "conj_list(some97,some96)". + "append(some88,some92,some98)". + "makevars([some94,some97],[some99,some100],beta(some98))". +} => { + _:sk_99 <= _:sk_100. +}. +{ + ?U_101 ?U_102. + "call((getlist(some101,some103),is_list(some103),is_graph(some102),conj_list(some102,some104),makevars(some102,some105,beta(some103)),(some105=''(some106,false),some107=true;catch(call(some105),some108,false),some107=some105),(some105=''(some109,some110)->some111=''(some112,some110);some111=some105)))". + (?U_107 { + ?U_113 ?U_111. + }) true. +} => false. +{ + ?U_114 :knows :Albert. +} => { + ?U_114 :knows :Kurt. }. { :e :p :a. @@ -21,38 +136,38 @@ _:e_x_1 :says { }. { { - ?U_5 :p :a. + ?U_118 :p :a. } => { - ?U_5 :q :b. + ?U_118 :q :b. }. } => { { - ?U_5 :r :c. + ?U_118 :r :c. } => { - ?U_5 :s :d. + ?U_118 :s :d. }. }. { - ?U_2 :p :o. + ?U_115 :p :o. } => { - ?U_2 :pp { - ?U_2 :ppp :ooo. + ?U_115 :pp { + ?U_115 :ppp :ooo. }. }. { - ?U_3 :p :o. + ?U_116 :p :o. } => { { { - ?U_3 :p2 ?U_6. + ?U_116 :p2 ?U_119. } => { - ?U_3 :p3 ?U_6. + ?U_116 :p3 ?U_119. }. } => { { - ?U_3 :p4 ?U_6. + ?U_116 :p4 ?U_119. } => { - ?U_3 :p5 ?U_6. + ?U_116 :p5 ?U_119. }. }. }. @@ -63,17 +178,17 @@ _:e_x_1 :says { }. { { - :s :p2 ?U_7. + :s :p2 ?U_120. } => { - :s :p3 ?U_7. + :s :p3 ?U_120. }. } => { { - :s :p4 ?U_7. + :s :p4 ?U_120. } => { - :s :p5 ?U_7. + :s :p5 ?U_120. }. }. { - ?U_4 :loves _:e_y_1. + ?U_117 :loves _:e_y_1. } <= true. diff --git a/reasoning/pack/out.n3 b/reasoning/pack/out.n3 index 4aa0f830e..43671f1ce 100644 --- a/reasoning/pack/out.n3 +++ b/reasoning/pack/out.n3 @@ -1,4 +1,4 @@ @prefix : . -:a :b _:e_c_148. -:u :v _:e_c_164. +:a :b _:e_c_1. +:u :v _:e_c_1. diff --git a/reasoning/rdfsurfaces/README b/reasoning/rdfsurfaces/README new file mode 100644 index 000000000..92ad753ab --- /dev/null +++ b/reasoning/rdfsurfaces/README @@ -0,0 +1,15 @@ +------------------ +Web Logic examples +------------------ + +See https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk +and https://github.com/w3c-cg/rdfsurfaces + +The top level surface is an implicit positive surface with implicit graffiti. + +log:nand is a negative surface used to express NAND based logic: +- nand (not and) is a log:onNegativeSurface +- negation is a log:onNegativeSurface +- disjunction is a log:onNegativeSurface containing only log:onNegativeSurface's +- => is a log:onNegativeSurface containing a log:onNegativeSurface +- <= is a log:onNegativeSurface containing a log:onNegativeSurface of a triple term diff --git a/reasoning/rdfsurfaces/beetle.n3 b/reasoning/rdfsurfaces/beetle.n3 new file mode 100644 index 000000000..ad61f7b36 --- /dev/null +++ b/reasoning/rdfsurfaces/beetle.n3 @@ -0,0 +1,45 @@ +# -------------- +# Beetle example +# -------------- +# +# See https://en.wikipedia.org/wiki/Disjunction_elimination + +@prefix log: . +@prefix : <#>. + +# beetle is a car +:beetle a :Car. + +# all cars are green or blue +(_:A) log:nand { + _:A a :Car. + () log:nand { + _:A :is :green. + }. + () log:nand { + _:A :is :blue. + }. +}. + +# green things are beautiful +(_:A) log:nand { + _:A :is :green. + () log:nand { + _:A :is :beautiful. + }. +}. + +# blue things are beautiful +(_:A) log:nand { + _:A :is :blue. + () log:nand { + _:A :is :beautiful. + }. +}. + +# query +{ + ?S :is ?O. +} log:query { + ?S :is ?O. +}. diff --git a/reasoning/rdfsurfaces/beetle6.n3 b/reasoning/rdfsurfaces/beetle6.n3 new file mode 100644 index 000000000..9c547048b --- /dev/null +++ b/reasoning/rdfsurfaces/beetle6.n3 @@ -0,0 +1,55 @@ +@prefix log: . +@prefix : <#>. + +# beetle is a car +:beetle a :Car. + +# all cars are green or blue +(_:A) log:nand { + _:A a :Car. + () log:nand { + _:A :is :green. + }. + () log:nand { + _:A :is :blue. + }. +}. + +# green things are nice or pretty +(_:A) log:nand { + _:A :is :green. + () log:nand { + _:A :is :nice. + }. + () log:nand { + _:A :is :pretty. + }. +}. +# pretty things are beautiful +(_:A) log:nand { + _:A :is :pretty. + () log:nand { + _:A :is :beautiful. + }. +}. + +# cars are not beautiful +(_:A) log:nand { + _:A a :Car. + _:A :is :beautiful. +}. + +# blue things are beautiful +(_:A) log:nand { + _:A :is :blue. + () log:nand { + _:A :is :beautiful. + }. +}. + +# query +{ + ?S :is ?O. +} log:query { + ?S :is ?O. +}. diff --git a/reasoning/rdfsurfaces/output/beetle.n3 b/reasoning/rdfsurfaces/output/beetle.n3 new file mode 100644 index 000000000..7a17107e7 --- /dev/null +++ b/reasoning/rdfsurfaces/output/beetle.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:beetle :is :beautiful. diff --git a/reasoning/rdfsurfaces/output/beetle6.n3 b/reasoning/rdfsurfaces/output/beetle6.n3 new file mode 100644 index 000000000..19c081a46 --- /dev/null +++ b/reasoning/rdfsurfaces/output/beetle6.n3 @@ -0,0 +1,4 @@ +@prefix : . + +:beetle :is :green. +:beetle :is :nice. diff --git a/reasoning/rdfsurfaces/output/slide32.n3 b/reasoning/rdfsurfaces/output/slide32.n3 new file mode 100644 index 000000000..0838d4adf --- /dev/null +++ b/reasoning/rdfsurfaces/output/slide32.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:Ghent a :HumanCommunity. diff --git a/reasoning/rdfsurfaces/output/slide33.n3 b/reasoning/rdfsurfaces/output/slide33.n3 new file mode 100644 index 000000000..70ac08871 --- /dev/null +++ b/reasoning/rdfsurfaces/output/slide33.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:xxx a :aaa. diff --git a/reasoning/rdfsurfaces/output/socrates.n3 b/reasoning/rdfsurfaces/output/socrates.n3 new file mode 100644 index 000000000..fe5c6e4b0 --- /dev/null +++ b/reasoning/rdfsurfaces/output/socrates.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:Socrates a :Mortal. diff --git a/reasoning/rdfsurfaces/output/syllogism.n3 b/reasoning/rdfsurfaces/output/syllogism.n3 new file mode 100644 index 000000000..2079e34a0 --- /dev/null +++ b/reasoning/rdfsurfaces/output/syllogism.n3 @@ -0,0 +1,3 @@ +@prefix : . + +:test :is true. diff --git a/reasoning/rdfsurfaces/slide32.n3 b/reasoning/rdfsurfaces/slide32.n3 new file mode 100644 index 000000000..e7919ef0c --- /dev/null +++ b/reasoning/rdfsurfaces/slide32.n3 @@ -0,0 +1,18 @@ +@prefix log: . +@prefix : <#>. + +:Ghent a :City. + +(_:x) log:nand { + _:x a :City. + () log:nand { + _:x a :HumanCommunity. + }. +}. + +# query +{ + :Ghent a :HumanCommunity. +} log:query { + :Ghent a :HumanCommunity. +}. diff --git a/reasoning/rdfsurfaces/slide33.n3 b/reasoning/rdfsurfaces/slide33.n3 new file mode 100644 index 000000000..cf175ee85 --- /dev/null +++ b/reasoning/rdfsurfaces/slide33.n3 @@ -0,0 +1,54 @@ +@prefix owl: . +@prefix log: . +@prefix : <#>. + +# slide 33 example from https://www.slideshare.net/PatHayes/blogic-iswc-2009-invited-talk + +# owl restriction +:aaa owl:onProperty :bbb. +:aaa owl:allValuesFrom :ccc. + +# the following 2 triples should entail :yyy a :ccc. +#:xxx a :aaa. +#:xxx :bbb :yyy. + +# the following codex should entail :xxx a :aaa. +(_:y) log:nand { + :xxx :bbb _:y. + () log:nand { + _:y a :ccc. + }. +}. + +# owl:allValuseFrom description logic +(_:a _:b _:c) log:nand { + _:a owl:onProperty _:b. + _:a owl:allValuesFrom _:c. + () log:nand { + (_:x _:y) log:nand { + _:x a _:a. + _:x _:b _:y. + () log:nand { + _:y a _:c. + }. + }. + (_:x) log:nand { + (_:y) log:nand { + _:x _:b _:y. + () log:nand { + _:y a _:c. + }. + }. + () log:nand { + _:x a _:a. + }. + }. + }. +}. + +# query +{ + :xxx a :aaa. +} log:query { + :xxx a :aaa. +}. diff --git a/reasoning/rdfsurfaces/socrates.n3 b/reasoning/rdfsurfaces/socrates.n3 new file mode 100644 index 000000000..c63c27569 --- /dev/null +++ b/reasoning/rdfsurfaces/socrates.n3 @@ -0,0 +1,27 @@ +# ------------------ +# Socrates inference +# ------------------ +# +# Infer that Socrates is mortal. + +@prefix rdfs: . +@prefix log: . +@prefix : <#>. + +:Socrates a :Human. +:Human rdfs:subClassOf :Mortal. + +(_:A _:B _:S) log:nand { + _:A rdfs:subClassOf _:B. + _:S a _:A. + () log:nand { + _:S a _:B. + }. +}. + +# query +{ + :Socrates a :Mortal. +} log:query { + :Socrates a :Mortal. +}. diff --git a/reasoning/rdfsurfaces/syllogism.n3 b/reasoning/rdfsurfaces/syllogism.n3 new file mode 100644 index 000000000..a4a5cbdc6 --- /dev/null +++ b/reasoning/rdfsurfaces/syllogism.n3 @@ -0,0 +1,78 @@ +@prefix log: . +@prefix : <#>. + +# Examples from "Neeltje Komt Dinsdag In Evakostuum" , M.C. Gomperts + +:Tweety a :Bird. + +## Syllogism 1 : Camestres + +# All cats are mammals +(_:Cat) log:nand { + _:Cat a :Cat. + () log:nand { + _:Cat a :Mammal. + }. +}. + +# No bird is a mammal +(_:Bird) log:nand { + _:Bird a :Bird. + _:Bird a :Mammal. +}. + +# IMPLIES: Bird is not a Cat + +## Syllogism 2 : Datasi + +# All cats are feline +(_:Cat) log:nand { + _:Cat a :Cat. + () log:nand { + _:Cat a :Feline. + }. +}. + +# Some cats are white +_:X a :Cat , :White. + +# IMPLIES : Some white are feline + +# Syllogism 3 : Ferio + +# No muslim is a christian +(_:M) log:nand { + _:M a :Muslim. + _:M a :Christian. +}. + +# Some worshippers are muslim +_:P a :Worshipper , :Muslim. + +# IMPLIES : Some worshipper is not a christian + +() log:nand { + # 1 + () log:nand { + :Tweety a :Cat. + }. + + # 2 + _:X a :White, :Feline. + + # 3 + () log:nand { + _:P a :Christian. + }. + + () log:nand { + :test :is true. + }. +}. + +# Test +{ + :test :is true. +} log:query { + :test :is true. +}. diff --git a/reasoning/rdfsurfaces/test b/reasoning/rdfsurfaces/test new file mode 100755 index 000000000..95f232220 --- /dev/null +++ b/reasoning/rdfsurfaces/test @@ -0,0 +1,6 @@ +#!/bin/bash +for f in *.n3 +do + echo + eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --nope $f --output output/$f + eye --quiet --skolem-genid 8b98b360-9a70-4845-b52c-c675af60ad01 --nope $f --output output/$f +done