Step | Formula | Justification | Bindings |
---|---|---|---|
1 | ... | parsing <time.n3> | |
2 | <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> . | erasure from step 1 | |
3 | ... | parsing <owl2.n3> | |
4 | :propertyDisjointWith a :SymmetricProperty . | erasure from step 3 | |
5 | ... | parsing <owlth.n3> | |
6 | @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . | erasure from step 5 | |
7 | ... | rule from step 6 applied to steps (2, 4) | {'p': u'<http://www.w3.org/2002/07/owl#propertyDisjointWith>', 'w': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'v': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'} |
8 | <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> . | erasure from step 7 | |
9 | <http://sw.opencyc.org/2009/04/07/concept/en/perceives> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> . | erasure from step 1 | |
10 | { <http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } log:includes {<http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . | built-in Axiom log:includes | |
11 | ... | parsing <badmeta.n3> | |
12 | [ a <http://sw.opencyc.org/2009/04/07/concept/en/AffixingSignature>; <http://sw.opencyc.org/2009/04/07/concept/en/objectActedOn> <http://example.org/1995/manifesto>; <http://sw.opencyc.org/2009/04/07/concept/en/performer> :Bob ]. | erasure from step 11 | |
13 | @forAll :DOC, :WHO . { [ a <http://sw.opencyc.org/2009/04/07/concept/en/AffixingSignature>; <http://sw.opencyc.org/2009/04/07/concept/en/objectActedOn> :DOC; <http://sw.opencyc.org/2009/04/07/concept/en/performer> :WHO ]. } log:implies {:DOC c:speaks_for :WHO . } . | erasure from step 11 | |
14 | ... | rule from step 13 applied to steps (12,) | {'DOC': u'<http://example.org/1995/manifesto>', 'WHO': u'<badmeta.n3#Bob>', '_g_L40C8': '[...]'} |
15 | <http://example.org/1995/manifesto> c:speaks_for :Bob . | erasure from step 14 | |
16 | ... | parsing <httpsocial.n3> | |
17 | :information s:subPropertyOf c:says . | erasure from step 16 | |
18 | { <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } log:includes {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . | built-in Axiom log:includes | |
19 | <http://example.org/1995/manifesto> :uri "http://example.org/1995/manifesto" . | built-in Axiom log:uri | |
20 | ( "http://example.org/1995/manifesto" "http://([^/]+)/" ) :search ( "example.org" ) . | built-in Axiom str:search | |
21 | <http://example.org/1995/manifesto> :uri "http://example.org/1995/manifesto" . | built-in Axiom log:uri | |
22 | ( :Q1 ) list:member :Q1 . | built-in Axiom list:member | |
23 | :A1 hs:messageEntity {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . }; ht:statusCodeNumber "200" . :C1 ht:requests ( :Q1 ) . :Q1 ht:absoluteURI "http://example.org/1995/manifesto"; ht:methodName "GET"; ht:resp :A1 . | erasure from step 11 | |
24 | ... | parsing <httpspeech.n3> | |
25 | @forAll hs:E, hs:RES, :A, :CONNECTION, :I, :Q . { hs:RES log:uri :I . :A hs:messageEntity hs:E; ht:statusCodeNumber "200" . :CONNECTION ht:requests [ list:member :Q ] . :Q ht:absoluteURI :I; ht:methodName "GET"; ht:resp :A . } log:implies {:CONNECTION c:says {hs:RES hs:information hs:E . } . } . | erasure from step 24 | |
26 | ... | rule from step 25 applied to steps (21, 22, 23) | {'A': u'<badmeta.n3#A1>', 'E': '{2}', 'I': '"http...esto"', 'RES': u'<http://example.org/1995/manifesto>', 'Q': u'<badmeta.n3#Q1>', 'CONNECTION': u'<badmeta.n3#C1>', '_g_L134C29': '?'} |
27 | :C1 c:says {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . | erasure from step 26 | |
28 | :C1 ht:connectionAuthority "example.org" . | erasure from step 11 | |
29 | @forAll :E, :RES, htt:A, htt:CONNECTION, htt:I . { ( htt:I "http://([^/]+)/" ) str:search ( htt:A ) . :RES log:uri htt:I . htt:CONNECTION c:says {:RES :information :E . }; ht:connectionAuthority htt:A . } log:implies {htt:CONNECTION c:controls_spo ( :RES :information :E ) . } . | erasure from step 24 | |
30 | ... | rule from step 29 applied to steps (19, 20, 27, 28) | {'I': '"http...esto"', 'A': '"exam....org"', 'CONNECTION': u'<badmeta.n3#C1>', 'E': '{2}', 'RES': u'<http://example.org/1995/manifesto>'} |
31 | :C1 c:controls_spo ( <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } ) . | erasure from step 30 | |
32 | :C1 c:says {<http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . } . | erasure from step 26 | |
33 | ... | parsing <speech.n3> | |
34 | @forAll :obj, :pred, :subj, spe:A . { spe:A :controls_spo ( :subj :pred :obj ); :says [ log:includes {:subj :pred :obj . } ] . } log:implies {:subj :pred :obj . } . | erasure from step 33 | |
35 | ... | rule from step 34 applied to steps (18, 31, 32) | {'_g_L76C11': '{manifesto hs:information {2}}', 'subj': u'<http://example.org/1995/manifesto>', 'obj': '{2}', 'A': u'<badmeta.n3#C1>', 'pred': u'<httpspeech#information>'} |
36 | <http://example.org/1995/manifesto> hs:information {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . | erasure from step 35 | |
37 | ... | parsing <rdfs-nice.n3> | |
38 | @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . | erasure from step 37 | |
39 | ... | rule from step 38 applied to steps (17, 36) | {'_g_L71C8': u'<httpspeech#information>', 'xxx': u'<http://example.org/1995/manifesto>', 'yyy': '{2}', 'bbb': u'<speech#says>'} |
40 | <http://example.org/1995/manifesto> c:says {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . | erasure from step 39 | |
41 | @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . | erasure from step 33 | |
42 | ... | rule from step 41 applied to steps (15, 40) | {'A': u'<http://example.org/1995/manifesto>', 's': '{2}', 'B': u'<badmeta.n3#Bob>'} |
43 | :Bob c:says {<http://example.org/1995/manifesto> <http://purl.org/dc/elements/1.1/creator> :Bob . <http://penguin-house.example/2008/article2> <http://purl.org/dc/elements/1.1/source> <http://example.org/1995/manifesto> . } . | erasure from step 42 | |
44 | @forAll :SOMEONE, :SOURCE, :WORK . { :SOMEONE c:says [ log:includes {:WORK <http://purl.org/dc/elements/1.1/source> :SOURCE . } ] . } log:implies {:SOMEONE <http://sw.opencyc.org/2009/04/07/concept/en/perceives> :WORK . } . | erasure from step 11 | |
45 | ... | rule from step 44 applied to steps (10, 43) | {'_g_L48C24': '{2}', 'WORK': u'<http://penguin-house.example/2008/article2>', 'SOMEONE': u'<badmeta.n3#Bob>', 'SOURCE': u'<http://example.org/1995/manifesto>'} |
46 | :Bob <http://sw.opencyc.org/2009/04/07/concept/en/perceives> <http://penguin-house.example/2008/article2> . | erasure from step 45 | |
47 | @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . | erasure from step 37 | |
48 | ... | rule from step 47 applied to steps (9, 46) | {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/perceives>', 'xxx': u'<badmeta.n3#Bob>', 'yyy': u'<http://penguin-house.example/2008/article2>', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>'} |
49 | :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> <http://penguin-house.example/2008/article2> . | erasure from step 48 | |
50 | "2006-01-23" :lessThan "2008-05-16" . | built-in Axiom str:lessThan | |
51 | @forSome :_g22, :_g23 . :_g22 xsd:date "2008-05-16" . :_g23 xsd:date "2006-01-23" . | erasure from step 11 | |
52 | @forSome :_g22 . <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO> :_g22 . | erasure from step 11 | |
53 | <http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> . | erasure from step 1 | |
54 | @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . | erasure from step 37 | |
55 | ... | rule from step 54 applied to steps (52, 53) | {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/publicationDate_IBO>', 'xxx': u'<http://penguin-house.example/2008/article2>', 'yyy': '[...]', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf>'} |
56 | @forSome :_g22 . <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> :_g22 . | erasure from step 55 | |
57 | @forSome :_g23 . bad:Bob <http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath> :_g23 . | erasure from step 11 | |
58 | <http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath> :subPropertyOf <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> . | erasure from step 1 | |
59 | @forAll :bbb, :xxx, :yyy . { @forSome run:_g21 . run:_g21 s:subPropertyOf :bbb . :xxx run:_g21 :yyy . } log:implies {:xxx :bbb :yyy . } . | erasure from step 37 | |
60 | ... | rule from step 59 applied to steps (57, 58) | {'_g_L71C8': u'<http://sw.opencyc.org/2009/04/07/concept/en/dateOfDeath>', 'xxx': u'<badmeta.n3#Bob>', 'yyy': '[...]', 'bbb': u'<http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf>'} |
61 | @forSome :_g23 . bad:Bob <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> :_g23 . | erasure from step 60 | |
62 | @forAll :TMAX, :TMIN, :TOBJ1, :TOBJ2 . { :TMAX str:lessThan :TMIN . :TOBJ1 <http://sw.opencyc.org/2009/04/07/concept/en/endsNoLaterThanEndingOf> [ xsd:date :TMAX ] . :TOBJ2 <http://sw.opencyc.org/2009/04/07/concept/en/startsNoEarlierThanStartingOf> [ xsd:date :TMIN ] . } log:implies {:TOBJ1 <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :TOBJ2 . } . | erasure from step 1 | |
63 | ... | rule from step 62 applied to steps (50, 51, 56, 61) | {'TMIN': '"2008...5-16"', 'TOBJ1': u'<badmeta.n3#Bob>', 'TOBJ2': u'<http://penguin-house.example/2008/article2>', 'TMAX': '"2006...1-23"', '_g_L51C43': '[...]', '_g_L50C37': '[...]'} |
64 | :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> <http://penguin-house.example/2008/article2> . | erasure from step 63 | |
65 | @forAll :P, :X, :Y, :Z . { @forSome run:_g20 . run:_g20 owl:propertyDisjointWith :P . :X run:_g20 :Y; :P :Z . } log:implies {:Y owl:differentFrom :Z . } . | erasure from step 3 | |
66 | ... | rule from step 65 applied to steps (8, 49, 64) | {'Y': u'<http://penguin-house.example/2008/article2>', 'X': u'<badmeta.n3#Bob>', 'Z': u'<http://penguin-house.example/2008/article2>', '_g_L12C6': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'P': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'} |
67 | <http://penguin-house.example/2008/article2> :differentFrom <http://penguin-house.example/2008/article2> . | erasure from step 66 | |
68 | ... | parsing <contradiction.n3> | |
69 | @forAll :X . { :X owl:differentFrom :X . } log:implies {:X owl:differentFrom :X . } . | erasure from step 68 | |
70 | ... | rule from step 69 applied to steps (67,) | {'X': u'<http://penguin-house.example/2008/article2>'} |
71 | <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :propertyDisjointWith <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> . | erasure from step 7 | |
72 | <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> a :SymmetricProperty . | erasure from step 1 | |
73 | :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> <http://penguin-house.example/2008/article2> . | erasure from step 48 | |
74 | @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . | erasure from step 5 | |
75 | ... | rule from step 74 applied to steps (72, 73) | {'p': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'w': u'<http://penguin-house.example/2008/article2>', 'v': u'<badmeta.n3#Bob>'} |
76 | <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects> :Bob . | erasure from step 75 | |
77 | <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> a :SymmetricProperty . | erasure from step 1 | |
78 | :Bob <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> <http://penguin-house.example/2008/article2> . | erasure from step 63 | |
79 | @forAll :p, :v, :w . { :p a owl:SymmetricProperty . :v :p :w . } log:implies {:w :p :v . } . | erasure from step 5 | |
80 | ... | rule from step 79 applied to steps (77, 78) | {'p': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>', 'w': u'<http://penguin-house.example/2008/article2>', 'v': u'<badmeta.n3#Bob>'} |
81 | <http://penguin-house.example/2008/article2> <http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint> :Bob . | erasure from step 80 | |
82 | @forAll :P, :X, :Y, :Z . { @forSome run:_g20 . run:_g20 owl:propertyDisjointWith :P . :X run:_g20 :Y; :P :Z . } log:implies {:Y owl:differentFrom :Z . } . | erasure from step 3 | |
83 | ... | rule from step 82 applied to steps (71, 76, 81) | {'Y': u'<badmeta.n3#Bob>', 'X': u'<http://penguin-house.example/2008/article2>', 'Z': u'<badmeta.n3#Bob>', '_g_L12C6': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyIntersects>', 'P': u'<http://sw.opencyc.org/2009/04/07/concept/en/temporallyDisjoint>'} |
84 | :Bob owl:differentFrom :Bob . | erasure from step 83 | |
85 | @forAll :X . { :X owl:differentFrom :X . } log:implies {:X owl:differentFrom :X . } . | erasure from step 68 | |
86 | ... | rule from step 85 applied to steps (84,) | {'X': u'<badmeta.n3#Bob>'} |
87 | :Bob owl:differentFrom :Bob . <http://penguin-house.example/2008/article2> owl:differentFrom <http://penguin-house.example/2008/article2> . | conjoining steps (70, 86) |
Conclusion:
@prefix : <badmeta.n3#> . @prefix owl: <http://www.w3.org/2002/07/owl#> . :Bob owl:differentFrom :Bob . <http://penguin-house.example/2008/article2> owl:differentFrom <http://penguin-house.example/2008/article2> .