For an application in declarative knowledge representation, I am interested in formal explanations within Datalog programs, which are essentially proof trees.
This is exactly the same proof tree navigation problem discussed by Wlodek Drabent in his work on declarative debugging, which the ddebug pack implements very concisely and with a very clean interface (thank you very much for that, Jan!).
The one issue for my specific use case is that while Wlodek’s original code (only circulated privately, as far I know) treated negative goals as leaves in the tree, the implementation in the ddebug pack seems to omit them entirely. For instance, for the example
passable(X,Y) :-
adjacent(X,Y),
\+ barrier(X,Y).
adjacent(a,b).
adjacent(b,c).
barrier(b,c).
querying ddebug(passable(a,b)) results in
<root>
% /home/weitkaemper/Logic_Programming/Causality/SWI/definatory_causal_models/ddtest.pl:1
passable(a,b) :-
[1] adjacent(a,b).
while Wlodek’s navigator would show \+ barrier(a,b) as an additional leaf of the tree.
Since in the framework of causal logic I am working in, formal explanations correspond to proof trees in which negations are true by default and therefore do not require a further explanation, the latter behaviour would capture what I need perfectly.
Unfortunately, as a non-SWI expert the implementation using debug hooks is difficult for me to adapt to try and achieve this behaviour myself. On the other hand, Wlodek’s implementation using program transformation on a file level is inconvenient for me since my application deals with dynamically asserted clauses.
Any assistance would be greatly appreciated!