{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T20:57:26Z","timestamp":1780952246504,"version":"3.54.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["175281"],"award-info":[{"award-number":["175281"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["FW-HTF 2129008"],"award-info":[{"award-number":["FW-HTF 2129008"]}]},{"name":"National Science Foundation","award":["CA-HDR 2033558"],"award-info":[{"award-number":["CA-HDR 2033558"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>\n                    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,\n                    <jats:italic toggle=\"yes\">debugging<\/jats:italic>\n                    it is hard, even for experts. When proof search cannot prove the goal, the programmer\u2019s best source of information is a massive AND\u2013OR graph representing the tool\u2019s 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.\n                  <\/jats:p>\n                  <jats:p>We propose a new formulation of proof search debugging, which: (i)\u00a0views AND\u2013OR graphs as a partial representations of the underlying proof system, (ii)\u00a0treats debugging as a process of applying modifications to this proof system, and (iii)\u00a0uses 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 \u201cwhy-not\u201d debugging strategies as well as new strategies, and we evaluate such strategies on 284 AND\u2013OR graphs. We find that a strategy that enforces a property called Strong Soundness reduces the number of decisions by 1.4\u00d7\u20133.2\u00d7 compared to an unsound baseline, and a new property we call Strong Completeness Modulo Observability enables pruning to further reduce decisions by 1.0\u00d7\u20132.8\u00d7 for an overall reduction of 2.0\u00d7\u20133.8\u00d7.<\/jats:p>","DOI":"10.1145\/3808344","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"2427-2451","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Navigating AND\u2013OR Graph Modifications to Debug Failing Proof Search"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2311-1873","authenticated-orcid":false,"given":"Justin","family":"Lubin","sequence":"first","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-1087-0995","authenticated-orcid":false,"given":"Marlena","family":"Preigh","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8066-4218","authenticated-orcid":false,"given":"Max","family":"Willsey","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0557-3580","authenticated-orcid":false,"given":"Sarah E.","family":"Chasins","sequence":"additional","affiliation":[{"name":"University of California at Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57530-8_7"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74565-5_7"},{"key":"e_1_2_2_4_1","unstructured":"Anthony Bargnesi Anselmo DiFabio William Hayes Georgiy Shibaev (@RangerMauve on Github) Cristophe Benz Hugh Pyle @erik470 on Github and Travis Giggy. 2021. JSON Graph Format (JGF). https:\/\/web.archive.org\/web\/20251110001441\/https:\/\/jsongraphformat.info\/ Accessed: 2025-11-09"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44503-X_20"},{"key":"e_1_2_2_7_1","volume-title":"Understanding the Control Flow of Prolog Programs. In Logic Programing Workshop.","author":"Byrd Lawrence","year":"1980","unstructured":"Lawrence Byrd. 1980. Understanding the Control Flow of Prolog Programs. In Logic Programing Workshop."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.035"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88594-8_8"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_9"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Rafael Caballero Adri\u00e1n Riesco and Josep Silva. 2017. A Survey of Algorithmic Debugging. In ACM Computing Surveys (CSUR). https:\/\/doi.org\/10.1145\/3106740 10.1145\/3106740","DOI":"10.1145\/3106740"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559845.1559901"},{"key":"e_1_2_2_13_1","unstructured":"Akira Charoensit David Carral Pierre Bisquert Lucas Rouquette and Federico Ulliana. 2024. Rule-Aware Datalog Fact Explanation Using Group-SAT Solver. In RuleML+RR."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535863"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507659"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/047174882X"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-7373(86)80020-7"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10036-5"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","unstructured":"Marc Eisenstadt and Mike Brayshaw. 1988. The Transparent PROLOG Machine (TPM): An Execution Model and Graphical Debugger for Logic Programming. In The Journal of Logic Programming. issn:0743-1066 https:\/\/doi.org\/10.1016\/0743-1066(88)90001-5 10.1016\/0743-1066(88)90001-5","DOI":"10.1016\/0743-1066(88)90001-5"},{"key":"e_1_2_2_20_1","unstructured":"Thom Fruehwirth Jan Wielemaker and Leslie De Koninck. 2012. SWI Prolog Reference Manual 6.2.2. https:\/\/web.archive.org\/web\/20251009164929\/https:\/\/eu.swi-prolog.org\/pldoc\/man?section=debugoverview isbn:978-3-8482-2617-7 Accessed 2025-11-08"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC58990.2023.00029"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729302"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1265530.1265535"},{"key":"e_1_2_2_24_1","unstructured":"Brian Hempel. 2019. Compendium of OS and PL working hypotheses and questions. https:\/\/web.archive.org\/web\/20191102080532\/https:\/\/people.cs.uchicago.edu\/ brianhempel\/compendium.html Accessed: 2025-11-08"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.14778\/1453856.1453936"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2025.15"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512649"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","unstructured":"Sven K\u00f6hler Bertram Lud\u00e4scher and Yannis Smaragdakis. 2012. Declarative Datalog Debugging for Mere Mortals. In International Datalog 2.0 Workshop. https:\/\/doi.org\/10.1007\/978-3-642-32925-8_12 10.1007\/978-3-642-32925-8_12","DOI":"10.1007\/978-3-642-32925-8_12"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.14778\/3229863.3236233"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-018-0518-5"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.19007039"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.19665844"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.19006570"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729264"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622824"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55460-2_32"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386005"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3138818"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/WVL.1991.238854"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1192.001.0001"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","unstructured":"Josep Silva. 2011. A Survey on Algorithmic Debugging Strategies. In Advances in Engineering Software. https:\/\/doi.org\/10.1016\/j.advengsoft.2011.05.024 10.1016\/j.advengsoft.2011.05.024","DOI":"10.1016\/j.advengsoft.2011.05.024"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_5"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/871895.871903"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017486"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512648"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48166-4_16"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535870"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738009"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3379446"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808344","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808344","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T19:57:57Z","timestamp":1780948677000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808344"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":53,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808344"],"URL":"https:\/\/doi.org\/10.1145\/3808344","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}