Semi-intelligible Isar proofs from machine-generated proofs
From MaRDI portal
Publication:287340
DOI10.1007/S10817-015-9335-3zbMATH Open1356.68178OpenAlexW1216298300WikidataQ113901251 ScholiaQ113901251MaRDI QIDQ287340FDOQ287340
Albert Steckermeier, Jasmin Christian Blanchette, Mathias Fleury, Sascha Böhme, Steffen Juilf Smolka
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01211748/file/paper.pdf
Recommendations
Cites Work
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Satallax: An Automatic Higher-Order Prover
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- System Description: E 1.8
- PRocH: Proof Reconstruction for HOL Light
- Title not available (Why is that?)
- Reducibility among Combinatorial Problems
- Untersuchungen über das logische Schliessen. I
- Property-directed incremental invariant generation
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Resolution theorem proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Lightweight relevance filtering for machine-generated resolution problems
- Obvious inferences
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- Equational reasoning in Isabelle
- On the rules of suppositions in formal logic
- Methods of lemma extraction in natural deduction proofs
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- SMT proof checking using a logical framework
- Translating higher-order clauses to first-order clauses
- Assertion-level proof representation with under-specification
- Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
- Automated Analysis of Regular Algebra
- More SPASS with Isabelle
- Improving legibility of natural deduction proofs is not trivial
- Concrete Semantics
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Title not available (Why is that?)
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computing Tiny Clause Normal Forms
- Ribbon Proofs for Separation Logic
- Encoding Monomorphic and Polymorphic Types
- MaSh: Machine Learning for Sledgehammer
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- Fast LCF-Style Proof Reconstruction for Z3
- Sledgehammer: Judgement Day
Cited In (14)
- Scalable fine-grained proofs for formula processing
- Mining the Archive of Formal Proofs
- Reliable reconstruction of fine-grained proofs in a proof assistant
- A verified SAT solver framework with learn, forget, restart, and incrementality
- CoSMed: a confidentiality-verified social media platform
- A learning-based fact selector for Isabelle/HOL
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Theorem proving as constraint solving with coherent logic
- Hammer for Coq: automation for dependent type theory
- A formal proof of the expressiveness of deep learning
- A formal proof of the expressiveness of deep learning
- VizAR: visualization of automated reasoning proofs (system description)
- Source-Level Proof Reconstruction for Interactive Theorem Proving
Uses Software
This page was built for publication: Semi-intelligible Isar proofs from machine-generated proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287340)
