source: doc/partial_proof @ 4a8f84a

The four Ws of partial proof

libabac, by default, would attempt to extract a partial proof 
if the initial fact query can not be proven. If the initial fact
query is found to be true, no partial proof will be attempted.

A fact query, "Can Coyote buy red rockets from Acme ?", is 
equivalent to attribute query fact, 

    "Acme.buy_rocket(red) <-?- Coyote".

When it is presented to YAP prolog db by libabac, it is translated 
into "isMember(pAcme,buy_rocket,red):-pCoyote" for assertion.

If the fact query can not be proven, libabac iterates through a 
sequence of actions in an attempt to discover partial proof 
related to the initial fact query.

We can break down the fact query into a general form,

   whom.what(whatwith) <-?- who

where 'whom' is the issuer principal, 'who' is the principal,
'what' is the role attribute and 'whatwith' is the parameter of
the attribute.

In the example fact query, 'whom' is Acme, 'who' is Coyote,
'what' is buy_rocket and red is assigned to 'whatwith'. 

In case, where such a fact can not be proven, one or more W 
terms are allowed to be uninstantiated and see what can be 
proven. 

Using the above example, the sequence libabac used to extract
partial proof is as follows,

case 1: acme.buy_rocket(red) <-?- coyote
        (Can Coyote buy red rockets from Acme?)
If no,
case 2: acme.What(Whatwith) <-?- coyote 
        (What with Whatwith can Coyote buy from Acme?)
If no,
case 2p: acme.What() <-?- coyote 
        (What can Coyote buy from Acme?)
If no,
case 3: acme.buy_rockets(red) <-?- Who
        (Who can buy red rockets from Acme?)
If no,
case 4: Whom.buy_rockets(red) <-?- coyote
        (From Whom can Coyote buy red rockets from?)
If no,
case 5: Whom.What(Whatwith) <-?- coyote
        (What with Whatwith can Coyote do from Whom?)

'whatwith' is in tandem with 'what', if there is no 'whatwith' 
term, then case 2p is skipped.

Multiple partial proofs can be extracted using next_proof() api 
call just like for fact proofs. It is possible to force libabac to
iterate through all the partial proof query cases listed above and
collect all the possible partial proofs. It is likely that there
will be duplication of proofs. No filtering will be done from libabac
side since each individual partial proof query is considered to be
independent from each other.

Note, the return code of abac_context_query() is such that success 
is only returned if the fact query is true. Even when there is a
returning partial proof, the return code will be false.