Sledgehammer: Judgement Day

DOI10.1007/978-3-642-14203-1_9zbMath1291.68327OpenAlexW1599039905MaRDI QIDQ5747754

Tobias Nipkow, Sascha Böhme

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

Mathematics Subject Classification ID

Related Items (36)

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 ⋮ A verified durable transactional mutex lock for persistent x86-TSO ⋮ 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

• SPASS
• Isar
• Sledgehammer
• E Theorem Prover
• SystemOnTPTP
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Sledgehammer: Judgement Day