Conference proceeding
An Interactive SMT Tactic in Coq using Abductive Reasoning
EPiC Series in Computing, Vol.94, pp.11-22
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
2023
DOI: 10.29007/432m
Abstract
A well-known challenge in leveraging automatic theorem provers, such as satisfiability modulo theories (SMT) solvers, to discharge proof obligations from interactive theorem provers (ITPs) is determining which axioms to send to the solver together with the con- jecture to be proven. Too many axioms may confuse or clog the solver, while too few may make a theorem unprovable. When a solver fails to prove a conjecture, it is unclear to the user which case transpired. In this paper we enhance SMTCoq — an integration between the Coq ITP and the cvc5 SMT solver — with a tactic called abduce aimed at mitigating the uncertainty above. When the solver fails to prove the goal, the user may invoke abduce which will use abductive reasoning to provide facts that will allow the solver to prove the goal, if any.
Details
- Title: Subtitle
- An Interactive SMT Tactic in Coq using Abductive Reasoning
- Creators
- Haniel Barbosa - Universidade Federal de Minas GeraisChantal Keller - Université Paris-SaclayAndrew Reynolds - University of Iowa, Computer ScienceArjun Viswanathan - University of IowaCesare Tinelli - University of Iowa, Computer ScienceClark Barrett - Stanford University
- Resource Type
- Conference proceeding
- Publication Details
- EPiC Series in Computing, Vol.94, pp.11-22
- Conference
- 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
- DOI
- 10.29007/432m
- ISSN
- 2398-7340
- eISSN
- 2398-7340
- Grant note
- This work was partially funded by Amazon Web Services, the Stanford Center for Automated Reasoning, and NSF grant #2019348.
- Language
- English
- Date published
- 2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984586040802771
Metrics
1 Record Views