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 verificationStone Relation AlgebrasMechanizing a process algebra for network protocolsA heuristic prover for real inequalitiesConflict-driven satisfiability for theory combination: lemmas, modules, and proofsReasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOLAn algebraic approach to computations with progressAutomatic Proof and Disproof in Isabelle/HOLRelation-Algebraic Verification of Prim’s Minimum Spanning Tree AlgorithmA Hierarchy of Algebras for Boolean SubsetsConstraint solving for finite model finding in SMT solversRandom Forests for Premise SelectionAn Axiomatic Value Model for Isabelle/UTPUnnamed ItemLearning-assisted theorem proving with millions of lemmasProgramming and verifying a declarative first-order prover in Isabelle/HOLAn algebraic approach to multirelations and their propertiesVerifying minimum spanning tree algorithms with Stone relation algebrasAlgebras for iteration and infinite computationsAn algebraic framework for minimum spanning tree problemsReliable reconstruction of fine-grained proofs in a proof assistantSledgehammerReasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point TheoremReconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOLInfinite executions of lazy and strict computationsExtending Sledgehammer with SMT solversLearning-assisted automated reasoning with \(\mathsf{Flyspeck}\)


Uses Software


Cites Work




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