  The theory revision problem is the problem of how best to go about revising a
deficient domain theory using information contained in examples that expose
inaccuracies. In this paper we present our approach to the theory revision
problem for propositional domain theories. The approach described here, called
PTR, uses probabilities associated with domain theory elements to numerically
track the ``flow'' of proof through the theory. This allows us to measure the
precise role of a clause or literal in allowing or preventing a (desired or
undesired) derivation for a given example. This information is used to
efficiently locate and repair flawed elements of the theory. PTR is proved to
converge to a theory which correctly classifies all examples, and shown
experimentally to be fast and accurate even for deep theories.
