Extending Sledgehammer with SMT solvers
From MaRDI portal
(Redirected from Publication:5200019)
Extending Sledgehammer with SMT solvers (scientific article; zbMATH DE number 5934346)
Extending Sledgehammer with SMT solvers (scientific article; zbMATH DE number 5934346)
Recommendations
Cites work
- A polymorphic intermediate verification language: design and logical encoding
- An introduction to mathematical logic and type theory: To truth through proof.
- Analytic tableaux for higher-order logic with choice
- Automated proof construction in type theory using resolution
- Automated Reasoning
- Combining superposition, sorts and splitting
- Computing small clause normal forms
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Fast LCF-Style Proof Reconstruction for Z3
- Handling Polymorphism in Automated Deduction
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- scientific article; zbMATH DE number 1614711 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1552511 (Why is no real title available?)
- scientific article; zbMATH DE number 2154400 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Lightweight relevance filtering for machine-generated resolution problems
- MPTP 0.2: Design, implementation, and initial experiments
- Property-directed incremental invariant generation
- Sine qua non for large theory reasoning
- Sledgehammer: judgement day
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Tools and Algorithms for the Construction and Analysis of Systems
- Translating higher-order clauses to first-order clauses
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
Cited in
(45)- An algebraic framework for minimum spanning tree problems
- Sledgehammer
- LEO-II and Satallax on the Sledgehammer test bench
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Extending SMT solvers to higher-order logic
- Infinite executions of lazy and strict computations
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Semi-intelligible Isar proofs from machine-generated proofs
- Mechanizing a process algebra for network protocols
- A heuristic prover for real inequalities
- Adding decision procedures to SMT solvers using axioms with triggers
- Random forests for premise selection
- An Axiomatic Value Model for Isabelle/UTP
- An algebraic approach to computations with progress
- 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
- Automatic proof and disproof in Isabelle/HOL
- Relation-algebraic verification of Prim's minimum spanning tree algorithm
- Constraint solving for finite model finding in SMT solvers
- SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
- Learning-assisted theorem proving with millions of lemmas
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
- A Hierarchy of Algebras for Boolean Subsets
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- An algebraic approach to multirelations and their properties
- Stone relation algebras
- Automating theorem proving with SMT
- Sledgehammer: judgement day
- A proof system for graph (non)-isomorphism verification
- Formalized proof systems for propositional logic
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Hammering Floating-Point Arithmetic
- Extending ACL2 with SMT solvers
- Reconstruction of SMT proofs with Lambdapi
- Hammering higher order set theory
- Faithful logic embeddings in HOL -- deep and shallow
- More is less: adding polynomials for faster explanations in NLSAT
- Linear termination is undecidable
- Algebras for iteration and infinite computations
- Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)
- Microeconomics and the First Welfare Theorem
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
Describes a project that uses
Uses Software
This page was built for publication: Extending Sledgehammer with SMT solvers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5200019)
