Step | Formula | Justification | Bindings |
---|---|---|---|
1 | ( :_g5 ) list:member :_g5 . | built-in Axiom list:member | |
2 | ... | parsing <mashup.n3> | |
3 | @forSome run:_g5 . :Q1 ht:headers ( run:_g5 ) . :bob :cookie "s3lkw3lij4wl3i" . run:_g5 ht:fieldName "Cookie"; ht:fieldValue "s3lkw3lij4wl3i" . | erasure from step 2 | |
4 | @forAll :COOKIE, :Q, :USER . { :Q ht:headers [ list:member [ ht:fieldName "Cookie"; ht:fieldValue :COOKIE ] ] . :USER ma:cookie :COOKIE . } log:implies {:Q c:speaks_for :USER . } . | erasure from step 2 | |
5 | ... | rule from step 4 applied to steps (1, 3) | {'Q': u'<mashup#Q1>', '_g_L89C33': '[...]', 'COOKIE': '"s3lk...wl3i"', 'USER': u'<mashup#bob>', '_g_L89C19': '?'} |
6 | :Q1 c:speaks_for :bob . | erasure from step 5 | |
7 | ( "&amount=1000000&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "amount" "1000000" "&for=mallory" ) . | built-in Axiom str:search | |
8 | ( "?account=bob&amount=1000000&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "account" "bob" "&amount=1000000&for=mallory" ) . | built-in Axiom str:search | |
9 | ( "http://bank.example/withdraw?account=bob&amount=1000000&for=mallory" "http:[^?]+(\?.*)" ) :search ( "?account=bob&amount=1000000&for=mallory" ) . | built-in Axiom str:search | |
10 | :Q1 ht:absoluteURI "http://bank.example/withdraw?account=bob&amount=1000000&for=mallory" . | erasure from step 2 | |
11 | @forAll :I, :PARAMS, :Q . { ( :I "http:[^?]+(\?.*)" ) str:search ( :PARAMS ) . :Q ht:absoluteURI :I . } log:implies {:Q ma:formParams :PARAMS . } . | erasure from step 2 | |
12 | ... | rule from step 11 applied to steps (9, 10) | {'I': '"http...lory"', 'Q': u'<mashup#Q1>', 'PARAMS': '"?acc...lory"'} |
13 | :Q1 :formParams "?account=bob&amount=1000000&for=mallory" . | erasure from step 12 | |
14 | @forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } . | erasure from step 2 | |
15 | ... | rule from step 14 applied to steps (8, 13) | {'Q': u'<mashup#Q1>', 'N': '"account"', 'PARAMS': '"?acc...lory"', 'REST': '"&amo...lory"', 'V': '"bob"'} |
16 | :Q1 :formParams "&amount=1000000&for=mallory" . | erasure from step 15 | |
17 | @forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } . | erasure from step 2 | |
18 | ... | rule from step 17 applied to steps (7, 16) | {'Q': u'<mashup#Q1>', 'N': '"amount"', 'PARAMS': '"&amo...lory"', 'REST': '"&for...lory"', 'V': '"1000000"'} |
19 | :Q1 :formParam [ :paramName "amount"; :paramValue "1000000" ] . | erasure from step 18 | |
20 | :bobAccount :accountName "bob" . :malloryAccount :accountName "mallory" . | erasure from step 2 | |
21 | ( "&for=mallory" "[?&]([^=]+)=([^&]+)(.*)" ) :search ( "for" "mallory" "" ) . | built-in Axiom str:search | |
22 | :Q1 :formParams "&for=mallory" . | erasure from step 18 | |
23 | @forAll :N, :PARAMS, :Q, :REST, :V . { ( :PARAMS "[?&]([^=]+)=([^&]+)(.*)" ) str:search ( :N :V :REST ) . :Q ma:formParams :PARAMS . } log:implies { @forSome run:_g6 . run:_g6 ma:paramName :N; ma:paramValue :V . :Q ma:formParam run:_g6; ma:formParams :REST . } . | erasure from step 2 | |
24 | ... | rule from step 23 applied to steps (21, 22) | {'Q': u'<mashup#Q1>', 'N': '"for"', 'PARAMS': '"&for...lory"', 'REST': '""', 'V': '"mallory"'} |
25 | :Q1 :formParam [ :paramName "for"; :paramValue "mallory" ] . | erasure from step 24 | |
26 | :Q1 :formParam [ :paramName "account"; :paramValue "bob" ] . | erasure from step 15 | |
27 | @forAll :A1, :A2, :AMT, mas:ACCT, mas:FOR, mas:Q . { :A1 :accountName mas:ACCT . :A2 :accountName mas:FOR . mas:Q :formParam [ :paramName "account"; :paramValue mas:ACCT ], [ :paramName "amount"; :paramValue :AMT ], [ :paramName "for"; :paramValue mas:FOR ] . } log:implies {mas:Q c:says {:A1 :debit :AMT . :A2 :credit :AMT . } . } . | erasure from step 2 | |
28 | ... | rule from step 27 applied to steps (19, 20, 25, 26) | {'A1': u'<mashup#bobAccount>', 'FOR': '"mallory"', '_g_L67C18': '[...]', '_g_L68C18': '[...]', 'Q': u'<mashup#Q1>', 'A2': u'<mashup#malloryAccount>', '_g_L66C18': '[...]', 'ACCT': '"bob"', 'AMT': '"1000000"'} |
29 | :Q1 c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . | erasure from step 28 | |
30 | ... | parsing <speech.n3> | |
31 | @forAll :A, :B, :s . { :A c:says :s; c:speaks_for :B . } log:implies {:B c:says :s . } . | erasure from step 30 | |
32 | ... | rule from step 31 applied to steps (6, 29) | {'A': u'<mashup#Q1>', 's': '{2}', 'B': u'<mashup#bob>'} |
33 | :bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . | erasure from step 32 | |
34 | ... | parsing <xsrf-goal.n3> | |
35 | { :bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . } log:implies {:bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . } . | erasure from step 34 | |
36 | :bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } . | rule from step 35 applied to steps (33,) | {} |
Conclusion:
@prefix : <mashup#> . @prefix c: <speech#> . :bob c:says {:bobAccount :debit "1000000" . :malloryAccount :credit "1000000" . } .