Extending Sledgehammer with SMT solvers

DOI10.1007/s10817-013-9278-5zbMath1314.68272OpenAlexW2022589543WikidataQ57382571 ScholiaQ57382571MaRDI QIDQ2351158

Sascha Böhme, Jasmin Christian Blanchette, Lawrence Charles Paulson

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-013-9278-5

zbMATH Keywords

SMT solversautomatic theorem proversinteractive theorem provers

Mathematics Subject Classification ID

Related Items (36)

A decision procedure for (co)datatypes in SMT solvers ⋮ Formalizing axiomatic systems for propositional logic in Isabelle/HOL ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ From informal to formal proofs in Euclidean geometry ⋮ Mining the Archive of Formal Proofs ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ A learning-based fact selector for Isabelle/HOL ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formalization of the resolution calculus for first-order logic ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Computer-Supported Exploration of a Categorical Axiomatization of Modeloids ⋮ Computer-Supported Analysis of Arguments in Climate Engineering ⋮ An automatically verified prototype of the Android permissions system ⋮ Isabelle formalisation of original representation theorems ⋮ Targeted configuration of an SMT solver ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Second-order properties of undirected graphs ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ Encoding Monomorphic and Polymorphic Types ⋮ Relational characterisations of paths ⋮ Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ From LCF to Isabelle/HOL ⋮ Towards satisfiability modulo parametric bit-vectors ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Model Finding for Recursive Functions in SMT ⋮ Automating Free Logic in Isabelle/HOL ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ A Vernacular for Coherent Logic ⋮ Theorem proving as constraint solving with coherent logic ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• HOL-Boogie
• Isabelle/HOL
• VAMPIRE
• SMT-LIB
• TPTP
• Yices
• Metis_
• cvc3
• z3
• ETPS
• HOL Light
• Sledgehammer
• VCC
• CVC Lite
• Gandalf
• E Theorem Prover
• Ivy
• SystemOnTPTP
• Jahob
• TRAMP
• Archive Formal Proofs
• Robbins Conjecture

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Property-directed incremental invariant generation
• Lightweight relevance filtering for machine-generated resolution problems
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• 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
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
• More SPASS with Isabelle
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Setoids in type theory
• Extending Sledgehammer with SMT Solvers
• Sine Qua Non for Large Theory Reasoning
• Integration of automated and interactive theorem proving in ILF
• Automated Reasoning
• Encoding Monomorphic and Polymorphic Types
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Fast LCF-Style Proof Reconstruction for Z3
• Sledgehammer: Judgement Day
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Extending Sledgehammer with SMT solvers