Thursday 31 March 2022, 2:00 PM, room 3U47 and online: Extending SMTCoq with Abductive Reasoning, Arjun Viswanathan (University of Iowa).

Interactive theorem provers (ITPs) such as Coq have various applications in proof formalization and software verification. They are used to produce rigorous computer-verified proofs of mathematical claims. Since proofs can be large and elaborate, a lot of efforts have been put recently into discharging proof obligations to automated theorem provers like SMT solvers. This requires some effort to maintain the correctness guarantees of the ITP, while using the less reliable SMT solver. SMTCoq is one such integration, that dispatches Coq goals to proof-producing SMT solvers and relies on computational reflection in Coq to check their proofs. In its current form, SMTCoq translates a proof goal from Coq to an unsatisfiability goal in the SMT solver and fails if it finds it to be satisfiable. The goal of our integration is that instead of simply failing to prove the formula, the SMT solver produces a hypothesis that would entail it. This is a reformulation of the abduction problem which, given a set of hypotheses H and goal G such that the H does not entail G, produces an abduct A that entails G, in conjunction with H. We further SMTCoq's integration with CVC4 by using its abduction solver to facilitate such an interaction between the Coq user and the SMT solver.