source: doc/partial_proof @ 97a6a36

mei_rt2mei_rt2_fix_1
Last change on this file since 97a6a36 was 646e57e, checked in by Mei <mei@…>, 12 years ago

1) add partial proof

  • Property mode set to 100644
File size: 2.4 KB
Line 
1
2The four Ws of partial proof
3
4Libabac, by default, would attempt to extract a partial proof
5if the initial fact query can not be proven. If the initial fact
6query is found to be true, no partial proof will be attempted.
7
8A fact query, "Can Coyote buy red rockets from Acme ?", is
9equivalent to attribute fact, "Acme.buy_rocket(red) <-?- Coyote".
10
11When it is presented to YAP prolog db by libabac, it is translated
12into "isMember(pAcme,buy_rocket,red):-pCoyote" for asserting.
13
14If the fact query can not be proven, libabac iterates through a
15sequence of actions in an attempt to discover partial proof
16related to the initial fact query.
17
18We can break down the fact query into a general form,
19
20   whom.what(whatwith) <-?- who
21
22where 'whom' is the issuer principal, 'who' is the principal,
23'what' is the role attribute and 'whatwith' is the parameter of
24the attribute.
25
26In the example fact query, 'whom' is Acme, 'who' is Coyote,'what'
27is buy_rocket and red is assigned to 'whatwith'.
28
29In case such a fact can not be proven, one or more W terms are
30allowed to be uninstantiated and see what can be proven.
31
32Using the above example, the sequence libabac used to extract
33partial proof is as follows,
34
35case 1: acme.buy_rocket(red) <-?- coyote
36        (Can Coyote buy red rockets from Acme?)
37If no,
38case 2: acme.What(Whatis) <-?- coyote
39        (What with Whatis can Coyote buy from Acme?)
40If no,
41case 2': acme.What() <-?- coyote
42        (What can Coyote buy from Acme?)
43If no,
44case 3: acme.buy_rockets(red) <-?- Who
45        (Who can buy red rockets from Acme?)
46If no,
47case 4: Whom.buy_rockets(red) <-?- coyote
48        (From Whom can Coyote buy red rockets from?)
49If no,
50case 5: Whom.What(Whatwith) <-?- coyote
51        (What with Whatwith can coyote do from Whom?)
52
53'whatwith' is in tandem with 'what', if there is no 'whatwith' term,
54then case 2' is skipped.
55
56Multiple partial proofs can be extracted using next_proof() api
57call just like for fact proofs. It is possible to force libabac to
58iterate through all the partial proof query cases listed above and
59collect all the possible partial proofs. It is likely that there
60will be duplication of proofs. No filtering will be done from libabac
61side since each individual partial proof query is considered to be
62independent from each other.
63
64Note, the return code of abac_context_query() is such that success
65is only returned if the fact query is true. Even when there is a
66returning partial proof, the return code will be false.
67
68
69
70
71   
72
73   
Note: See TracBrowser for help on using the repository browser.