The following pages link to Sledgehammer: Judgement Day (Q5747754):
Displaying 35 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- In praise of algebra (Q1941861) (← links)
- Superposition for full higher-order logic (Q2055874) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Automating change of representation for proofs in discrete mathematics (extended version) (Q2364883) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Encoding Monomorphic and Polymorphic Types (Q2974796) (← links)
- Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic (Q3179185) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- Cooperating Proof Attempts (Q3454105) (← links)
- Contextual Natural Deduction (Q3455860) (← links)
- (Q4989394) (← links)
- (Q5028488) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Mining State-Based Models from Proof Corpora (Q5495930) (← links)
- A light-weight integration of automated and interactive theorem proving (Q5741559) (← links)
- (Q5875442) (← links)
- Superposition with lambdas (Q5918381) (← links)
- Superposition with lambdas (Q5919500) (← links)
- Superposition for higher-order logic (Q6156638) (← links)
