Extending Sledgehammer with SMT Solvers

被引：0
|
作者：
Blanchette, Jasmin Christian [1 ]
Boehme, Sascha [1 ]
Paulson, Lawrence C. [2 ]
机构：
[1] Tech Univ Munich, Inst Informat, D-8000 Munich, Germany
[2] Univ Cambridge, Comp Lab, Cambridge CB2 1TN, England
来源：
AUTOMATED DEDUCTION - CADA-23 | 2011年 / 6803卷
基金：
英国工程与自然科学研究理事会;
关键词：
PROOF RECONSTRUCTION; SYSTEM DESCRIPTION; DESIGN; IMPLEMENTATION; VERIFICATION;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Sledgehammer is a component of Isabelle/HOL that employs 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. Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs' reach. Remarkably, the best SMT solver performs better than the best ATP on most of our benchmarks.
引用
收藏
页码：116 / +
页数：4
相关论文
共 50 条
  • [1] Extending Sledgehammer with SMT Solvers
    Blanchette, Jasmin Christian
    Boehme, Sascha
    Paulson, Lawrence C.
    [J]. JOURNAL OF AUTOMATED REASONING, 2013, 51 (01) : 109 - 128
  • [2] Extending Sledgehammer with SMT Solvers
    Jasmin Christian Blanchette
    Sascha Böhme
    Lawrence C. Paulson
    [J]. Journal of Automated Reasoning, 2013, 51 : 109 - 128
  • [3] Extending ACL2 with SMT Solvers
    Peng, Yan
    Greenstreet, Mark
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (192): : 61 - 77
  • [4] Extending SMT Solvers to Higher-Order Logic
    Barbosa, Haniel
    Reynolds, Andrew
    El Ouraoui, Daniel
    Tinelli, Cesare
    Barrett, Clark
    [J]. AUTOMATED DEDUCTION, CADE 27, 2019, 11716 : 35 - 54
  • [5] Extending SMT solvers with support for finite domain alldifferent constraint
    Milan Banković
    [J]. Constraints, 2016, 21 : 463 - 494
  • [6] Extending SMT solvers with support for finite domain alldifferent constraint
    Bankovic, Milan
    [J]. CONSTRAINTS, 2016, 21 (04) : 463 - 494
  • [7] Induction for SMT Solvers
    Reynolds, Andrew
    Kuncak, Viktor
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2015), 2015, 8931 : 80 - 98
  • [8] Extending the Scope of Translation Validation by Augmenting Path Based Equivalence Checkers with SMT Solvers
    Banerjee, Kunal
    Mandal, Chittaranjan
    Sarkar, Dipankar
    [J]. 18TH INTERNATIONAL SYMPOSIUM ON VLSI DESIGN AND TEST, 2014,
  • [9] Integrating SMT solvers in Rodin
    Deharbe, David
    Fontaine, Pascal
    Guyot, Yoann
    Voisin, Laurent
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2014, 94 : 130 - 143
  • [10] Symbolic Optimization with SMT Solvers
    Li, Yi
    Albarghouthi, Aws
    Kincaid, Zachary
    Gurfinkel, Arie
    Chechik, Marsha
    [J]. ACM SIGPLAN NOTICES, 2014, 49 (01) : 607 - 618
12345