Recommendations
Cites work
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- 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 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 2162299 (Why is no real title available?)
- Lightweight relevance filtering for machine-generated resolution problems
- MPTP 0.2: Design, implementation, and initial experiments
- Property-directed incremental invariant generation
- Reconstructing proofs at the assertion level
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Translating higher-order clauses to first-order clauses
Cited in
(43)- Introduction to ``Milestones in interactive theorem proving
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- In praise of algebra
- LEO-II and Satallax on the Sledgehammer test bench
- Superposition for full higher-order logic
- Reliable reconstruction of fine-grained proofs in a proof assistant
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Automating change of representation for proofs in discrete mathematics (extended version)
- AUTO2, a saturation-based heuristic prover for higher-order logic
- Semi-intelligible Isar proofs from machine-generated proofs
- Automating Induction with an SMT Solver
- Encoding monomorphic and polymorphic types
- Automatic proof and disproof in Isabelle/HOL
- Extracting a DPLL algorithm
- Implementation and evaluation of contextual natural deduction for minimal logic
- A learning-based fact selector for Isabelle/HOL
- Mining the Archive of Formal Proofs
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Cooperating proof attempts
- Contextual Natural Deduction
- Verification and code generation for invariant diagrams in Isabelle
- Superposition for lambda-free higher-order logic
- Fixed points theorems for non-transitive relations
- Extending Sledgehammer with SMT solvers
- A framework for developing stand-alone certifiers
- MaSh: machine learning for Sledgehammer
- Mining state-based models from proof corpora
- A light-weight integration of automated and interactive theorem proving
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Superposition with lambdas
- Superposition with lambdas
- Superposition for higher-order logic
- Hammering Floating-Point Arithmetic
- A verified durable transactional mutex lock for persistent x86-TSO
- Iterative monomorphisation
- Exploiting instantiations from paramodulation proofs in Isabelle/HOL
- Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity
- Linear termination is undecidable
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: Sledgehammer: judgement day
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747754)
