It also makes certain approaches to explainable AI rather
arbitrary. Like if you show just one SLD derivation as a justification
for a proof. I don’t know, whats your approach here:
A stack trace is just one proof of a main goal. But the same main goal
can have multiple proofs. In the parent thread an attempt was made by
the OP to use mode directed tabling, by a metric to find shortest proofs.
The problem is if a part of a such a proof gets invalidated, the main goal
might still have another proof path. So proof certificates give only a positive
answer to positive question, not a negative answer to a negative question,
They do not have the character of a categorical explanation, i.e. a unique explain.
So the notions stack trace, proof and search are all connected in SLD
Resolution, and it often gets overlooked that Prolog is a kind of non-determistic
language, which does search via backtracking, and that these objects are
not univalent or isomorphic for the same goal. Subgoaling is a rather
adventureaous exploration. It wouldn’t matter if you implement subgoaling
in Rust, or when DeepSeek Math shows subgoaling. It is still an exploration.
It also doesn’t matter when top-down Input Resolution is replaced by bottom-up
Unit Resolution, its still an exploration. And when a machine learning system
adopts Resolution, it adopts this explorative search. Yes or no?
P.S.: You see very clearly that proofs are not unique when you use
refutation methods, as in your algorithm 1 in your TOIL paper:
G, ~A |- f
The main goal is to find a contradiction f. While a contradiction is
even a domain independent formulation, it doesn’t contain any
predicates from the domain. You can say its one of the most unique
goals on earth that a resolution theorem prover could have. Yet
a theory G, ~A might have a multitude of root causes that cause
a contradiction. And even if you remove one root cause, there might
be still another root cause. But your proof search has arbitrarily stopped
at any of the existing root causes, that caused the contradiction.