Sledgehammer: judgement day
From MaRDI portal
Publication:5747754
Recommendations
Cites work
- 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?)
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- 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
(39)- In praise of algebra
- Extending Sledgehammer with SMT solvers
- Mining the Archive of Formal Proofs
- scientific article; zbMATH DE number 7471719 (Why is no real title available?)
- Introduction to ``Milestones in interactive theorem proving
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Extracting a DPLL algorithm
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Implementation and evaluation of contextual natural deduction for minimal logic
- Semi-intelligible Isar proofs from machine-generated proofs
- Superposition for higher-order logic
- Hammering Floating-Point Arithmetic
- Encoding monomorphic and polymorphic types
- Superposition for full higher-order logic
- Automating change of representation for proofs in discrete mathematics (extended version)
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Extending SMT solvers to higher-order logic
- A light-weight integration of automated and interactive theorem proving
- Automatic proof and disproof in Isabelle/HOL
- MaSh: machine learning for Sledgehammer
- AUTO2, a saturation-based heuristic prover for higher-order logic
- Automating Induction with an SMT Solver
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- LEO-II and Satallax on the Sledgehammer test bench
- Contextual Natural Deduction
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Superposition with lambdas
- Superposition with lambdas
- Extending Sledgehammer with SMT solvers
- A learning-based fact selector for Isabelle/HOL
- A framework for developing stand-alone certifiers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Cooperating proof attempts
- Mining state-based models from proof corpora
- A verified durable transactional mutex lock for persistent x86-TSO
- Verification and code generation for invariant diagrams in Isabelle
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)
