So, my post Progress? was snark and a bit insidery at that. Given that I’ve already had one person give me the puzzled comment about it, it seems right to give in and just dissect the damn frog already.
In ontology circles, esp. of the description logic variety, “explanation” is a key feature of knowledge based systems. Sometimes you hear the story of how the early expert system, Mycin, would diagnose with high reliability but doctors wouldn’t accept those diagnoses. Then they added an explanation facility and suddenly doctors would accept it. Thus, explanation is necessary to trust the system. (There’s actually some reasonable empirical evidence to show this for even modern expert systems, e.g., for financial analysis.)
Since early forms of explanation were essential “traces” of the system reasoning, it’s an easy step to say that explanations are “proofs”. This also hooks up with Hempel’s deductive nomological model of scientific explanation (i.e., a deductive argument with at least one scientific law as a premise).
However, when we talk ontology engineering, and esp. various debugging tasks, the most successful form of explanation has been so-called (and so-called by me, alas) justifications, that is, minimal subsets of the original theory which suffice for an entailment to hold.
Stefan Schlobach (and friends) almost certainly gets priority in the 2000, with loads of antecedents in and out of the DL community. Aditya, Evren, and I sorta reinvented them when trying to produce something from Pellet for the InferenceWeb system, and never looked back.
Borgida (the fellow I’m pretty sure I was quoting) had some work on explanation that was more proof oriented. This rather recent paper picks that up. At a DL workshop (where the first, more categorical paper was given) he got some push back (I’m pretty sure from me). The later paper is less categorical.
In the end, I really hope that people get away from the “Proofs are explanations, the best explanations, and the only explanations” mindset. I don’t think it’s fruitful.
On Facebook, Enrico again tried to frame everything in terms of proofs in some (perhaps varying) system or partial proof in a given system (the latter is super weak given we have decision procedures…every entailment has a finitely findable proof, so any string of lemmas is trivially convertible into a partial proof, in some sense).
But this is really analytically bogus. It’s unclear what benefit comes from reducing everything to proofs, partial or otherwise. (And what about model based explanations, esp. for non-entailments? Or analogical explanations such as with case based reasoning? And justifications really really are “just the premises”.) Does this clarify anything? Don’t we just reinvent the distinctions we want inside the framework (e.g., with partial proofs)? I certainly do not see how it would help Borgida et al, after all, there is no dialectical point in stressing that explanations are proofs when bolstering a fairly specific kind of proof as explanation if the first occurrence of proof provides almost no constraints.
In the end, I’ve no doubt that proofs can serve, even in the ontology engineering setting, some explanatory purposes. Heck, I’m researching them for these purposes! I also don’t much care if other people want to be blinkered, or want to bash justifications, or what have you, at least, I don’t see such bashing (directly or slyly) as substantive criticism. I do think it’s worth sitting down and trying to understand what such statements (or beliefs) actually buy us.
My current thought is “Not much, and probably are somewhat harmful.” I’m willing to be convinced otherwise if someone has the goods.