Navigating AND-OR Graph Modifications to Debug Failing Proof Search

Proof search powers our most advanced programming tools, from type systems, to search tactics for interactive theorem provers, to Datalog-backed program analyses. Although proof search tooling is powerful and now pervasive, debugging it is hard, even for experts. When proof search cannot prove the goal, the programmer's best source of information is a massive AND-OR graph representing the tool's internal state during the proof search process. The difficulty of understanding and debugging this vast trace of internal state locks programmers out of exactly the high-assurance automated reasoning tools we want them to adopt.

We propose a new formulation of proof search debugging, which: (i) views AND-OR graphs as a partial representations of the underlying proof system, (ii) treats debugging as a process of applying modifications to this proof system, and (iii) uses a debugging tool to solicit these modifications until the resulting proof system proves the original goal. This approach unifies decades of ad-hoc strategies in a single general-purpose framework and is applicable to the diverse range of programming tools that use proof search. Our framework can express existing "why-not" debugging strategies as well as new strategies, and we evaluate such strategies on 284 AND-OR graphs. We find that a strategy that enforces a property called Strong Soundness reduces the number of decisions by 1.4×-3.2× compared to an unsound baseline, and a new property we call Strong Completeness Modulo Observability enables pruning to further reduce decisions by 1.0×-2.8× for an overall reduction of 2.0×-3.8×. CCS Concepts: • Software and its engineering → Automatic programming.