Extending Sledgehammer with SMT Solvers
From MaRDI portal
Publication:5200019
DOI10.1007/978-3-642-22438-6_11zbMath1314.68271OpenAlexW1674186056WikidataQ57382606 ScholiaQ57382606MaRDI QIDQ5200019
Sascha Böhme, Jasmin Christian Blanchette, Lawrence Charles Paulson
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_11
Related Items (27)
A proof system for graph (non)-isomorphism verification ⋮ Stone Relation Algebras ⋮ Mechanizing a process algebra for network protocols ⋮ A heuristic prover for real inequalities ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ An algebraic approach to computations with progress ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Random Forests for Premise Selection ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Unnamed Item ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ An algebraic approach to multirelations and their properties ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ Algebras for iteration and infinite computations ⋮ An algebraic framework for minimum spanning tree problems ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Sledgehammer ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Infinite executions of lazy and strict computations ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MPTP 0.2: Design, implementation, and initial experiments
- Property-directed incremental invariant generation
- Lightweight relevance filtering for machine-generated resolution problems
- Isabelle/HOL. A proof assistant for higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- Automated proof construction in type theory using resolution
- Translating higher-order clauses to first-order clauses
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- Handling Polymorphism in Automated Deduction
- Sine Qua Non for Large Theory Reasoning
- Automated Reasoning
- Fast LCF-Style Proof Reconstruction for Z3
- Analytic Tableaux for Higher-Order Logic with Choice
- Sledgehammer: Judgement Day
- Tools and Algorithms for the Construction and Analysis of Systems
This page was built for publication: Extending Sledgehammer with SMT Solvers