Extending Sledgehammer with SMT Solvers

被引:78
作者
Blanchette, Jasmin Christian [1 ]
Boehme, Sascha [1 ]
Paulson, Lawrence C. [2 ]
机构
[1] Tech Univ Munich, Inst Informat, Munich, Germany
[2] Univ Cambridge, Comp Lab, Cambridge CB2 3QG, England
基金
英国工程与自然科学研究理事会;
关键词
SMT solvers; Automatic theorem provers; Interactive theorem provers; SYSTEM DESCRIPTION; PROOF RECONSTRUCTION; THEOREM PROVERS; VERIFICATION;
D O I
10.1007/s10817-013-9278-5
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs' reach.
引用
收藏
页码:109 / 128
页数:20
相关论文
共 62 条
[1]  
Ahrendt W, 1998, APPL LOG SER, V9, P97
[2]  
Andrews Peter B, 2002, APPL LOGIC, V27
[3]  
[Anonymous], 2019, LCP ISABELLE 2019
[4]  
[Anonymous], 6247 LNCS
[5]  
[Anonymous], 2006, YICES SMT SOLVER
[6]  
Armand Michael, 2011, Certified Programs and Proofs. Proceedings First International Conference, CPP 2011, P135
[7]  
Barrett C., 2010, The satisfiability modulo theories library (SMT-LIB)
[8]  
Barrett C, 2007, LECT NOTES COMPUT SC, V4590, P298
[9]  
Barsotti D, 2007, FORM ASP COMPUT, V19, P321, DOI 10.1007/S00165-007-0027-6
[10]   Setoids in type theory [J].
Barthe, G ;
Capretta, V ;
Pons, O .
JOURNAL OF FUNCTIONAL PROGRAMMING, 2003, 13 :261-293