Extending Sledgehammer with SMT Solvers
Extending Sledgehammer with SMT Solvers
复制标题
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Lawrence C. Paulson
中科院分区：
文献类型：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
Sledgehammer是Isabelle/HOL的一个组件，它采用基于分辨率的一阶自动定理证明器（ATP）来实现交互式证明中出现的目标。它以启发式的方式选择相关的事实，如果ATP是成功的，它会产生一个片段，在Isabelle中重放证明。我们扩展了Sledgehammer调用可满足性模理论（SMT）求解器，以及利用其相关过滤器和并行架构。ATP和SMT求解器很好地相互补充，Isabelle用户现在惊喜地发现SMT证明了ATP无法解决的问题。
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.
登录
查看更多内容
系统描述：TRAMP：在断言级别将机器发现的证明转换为 ND 证明
影响因子：
10.4
作者：
A. Meier
通讯作者：
A. Meier
Ωmega 的证明开发：(sqrt 2) 的非理性
DOI：
10.1007/978-94-017-0253-9_11
发表时间：
2003
期刊：
Automated Reasoning
影响因子：
--
作者：
J. Siekmann;Christoph Benzmüller;Armin Fiedler;A. Meier;I. Normann;Martin Pollet
通讯作者：
Martin Pollet
爱丁堡LCF
DOI：
--
发表时间：
1979
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
M. Gordon;R. Milner;C. P. Wadsworth
通讯作者：
C. P. Wadsworth
定理证明者合作：结合 HOL-Light 和 CVC Lite 的案例研究
DOI：
10.1016/j.entcs.2005.12.005
发表时间：
2005
期刊：
ArXiv
影响因子：
--
作者：
Sean McLaughlin;Clark W. Barrett;Yeting Ge
通讯作者：
Yeting Ge
整合甘道夫和 HOL
DOI：
10.1007/3-540-48256-3_21
发表时间：
1999
期刊：
ArXiv
影响因子：
--
作者：
Joe Hurd
通讯作者：
Joe Hurd