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