Sledgehammer: judgement day
From MaRDI portal
Publication:5747754
DOI10.1007/978-3-642-14203-1_9zbMATH Open1291.68327OpenAlexW1599039905MaRDI QIDQ5747754FDOQ5747754
Authors: Sascha Böhme, Tobias Nipkow 
Publication date: 14 September 2010
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.181.109
Recommendations
Cites Work
- Title not available (Why is that?)
- MPTP 0.2: Design, implementation, and initial experiments
- Title not available (Why is that?)
- Title not available (Why is that?)
- Property-directed incremental invariant generation
- Lightweight relevance filtering for machine-generated resolution problems
- Translating higher-order clauses to first-order clauses
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Reconstructing proofs at the assertion level
- Title not available (Why is that?)
Cited In (39)
- Extending Sledgehammer with SMT solvers
- Superposition with lambdas
- A framework for developing stand-alone certifiers
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Automating Induction with an SMT Solver
- Title not available (Why is that?)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Semi-intelligible Isar proofs from machine-generated proofs
- Contextual Natural Deduction
- Mining state-based models from proof corpora
- Mining the Archive of Formal Proofs
- Title not available (Why is that?)
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Superposition with lambdas
- Superposition for higher-order logic
- Extracting a DPLL algorithm
- Implementation and evaluation of contextual natural deduction for minimal logic
- Automating change of representation for proofs in discrete mathematics (extended version)
- Introduction to ``Milestones in interactive theorem proving
- Encoding monomorphic and polymorphic types
- A learning-based fact selector for Isabelle/HOL
- MaSh: machine learning for Sledgehammer
- Verification and code generation for invariant diagrams in Isabelle
- Superposition for full higher-order logic
- Extending SMT solvers to higher-order logic
- A light-weight integration of automated and interactive theorem proving
- Extending Sledgehammer with SMT solvers
- Cooperating proof attempts
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Hammering Floating-Point Arithmetic
- A verified durable transactional mutex lock for persistent x86-TSO
- Title not available (Why is that?)
- In praise of algebra
- Automatic proof and disproof in Isabelle/HOL
- AUTO2, a saturation-based heuristic prover for higher-order logic
- LEO-II and Satallax on the Sledgehammer test bench
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
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)
