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