9 Assumables

Assumables can be used for proof by contradiction or for abduction. Integrity constraints (rules that imply false) are handled specially in abduction. The interaction between assumables and negation as failure is not as general as it could be; for the goal ~g, any proof or partial proof of g should not depend on any assumables.

To to make an atom assumable, you can issue the command:

ailog: assumable atom.

When the atom is encountered, it is assumed to be true. The assumptions used to make a proof go though are collected and presented to the user when the answer is returned.

ailog: tell a(X) <- b(X) & c(X).
ailog: assumable c(X).
ailog: tell b(X) <- d(X) & e(X).
ailog: askable e(X).
ailog: tell d(a).
ailog: tell d(b).
ailog: tell d(c).
ailog: ask a(X).
Is e(a) true? [yes,no,unknown,why,help]: yes.
Answer: a(a).
Assuming: [c(a)].
  [more,ok,how,help]: more.
Is e(b) true? [yes,no,unknown,why,help]: no.
Is e(c) true? [yes,no,unknown,why,help]: yes.
Answer: a(c).
Assuming: [c(c)].
  [more,ok,how,help]: more.
No more answers.
ailog:

An explanation has to be consistent with the knowledge base. To say that some body is not true, you can use:

ailog: tell false <- body.

Here false is a special atom that is false in all models. Thus, this clause provides a constraint specifying that the body is false.

From the set of constraints, you need to create a set of nogoods to ensure that all explanations are consistent. To do this, you can issue the command:

ailog: create_nogoods.

The nogoods correspond to the sets of assumables that imply false.

To list all of the nogoods, you can issue the command:

ailog: nogoods.

To debug the nogoods, you can ask to prove false or ask whynot false.