Extending Sledgehammer with SMT Solvers

被引：0
|
作者：
Jasmin Christian Blanchette
Sascha Böhme
Lawrence C. Paulson
机构：
[1] Technische Universität München,Institut für Informatik
[2] University of Cambridge,Computer Laboratory
来源：
Journal of Automated Reasoning | 2013年 / 51卷
关键词：
SMT solvers; Automatic theorem provers; Interactive theorem provers;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：19
相关论文
共 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
    Blanchette, Jasmin Christian
    Boehme, Sascha
    Paulson, Lawrence C.
    [J]. AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 116 - +
  • [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