Sledgehammer: Judgement Day
From MaRDI portal
Publication:5747754
DOI10.1007/978-3-642-14203-1_9zbMath1291.68327OpenAlexW1599039905MaRDI QIDQ5747754
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
Related Items
Automating change of representation for proofs in discrete mathematics (extended version), Automating Induction with an SMT Solver, Semi-intelligible Isar proofs from machine-generated proofs, A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL, Automatic Proof and Disproof in Isabelle/HOL, Mining the Archive of Formal Proofs, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, Cooperating Proof Attempts, Extracting a DPLL Algorithm, Contextual Natural Deduction, Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic, A learning-based fact selector for Isabelle/HOL, Introduction to ``Milestones in interactive theorem proving, Unnamed Item, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, In praise of algebra, Superposition for higher-order logic, Unnamed Item, Encoding Monomorphic and Polymorphic Types, Unnamed Item, Verification and code generation for invariant diagrams in Isabelle, A framework for developing stand-alone certifiers, A light-weight integration of automated and interactive theorem proving, Extending Sledgehammer with SMT Solvers, Superposition with lambdas, Superposition with lambdas, Superposition for full higher-order logic, Reliable reconstruction of fine-grained proofs in a proof assistant, Extending SMT solvers to higher-order logic, AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic, Mining State-Based Models from Proof Corpora, Extending Sledgehammer with SMT solvers, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MPTP 0.2: Design, implementation, and initial experiments
- 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
- Reconstructing proofs at the assertion level
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
