Semi-intelligible Isar proofs from machine-generated proofs
From MaRDI portal
Publication:287340
DOI10.1007/s10817-015-9335-3zbMath1356.68178OpenAlexW1216298300WikidataQ113901251 ScholiaQ113901251MaRDI QIDQ287340
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
Related Items
Mining the Archive of Formal Proofs ⋮ A learning-based fact selector for Isabelle/HOL ⋮ CoSMed: a confidentiality-verified social media platform ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Hammer for Coq: automation for dependent type theory ⋮ VizAR: visualization of automated reasoning proofs (system description) ⋮ A formal proof of the expressiveness of deep learning ⋮ A formal proof of the expressiveness of deep learning ⋮ Scalable fine-grained proofs for formula processing ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Theorem proving as constraint solving with coherent logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Property-directed incremental invariant generation
- 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
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Equational reasoning in Isabelle
- Untersuchungen über das logische Schliessen. I
- 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
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- System Description: E 1.8
- Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
- Satallax: An Automatic Higher-Order Prover
- 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
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Computing Tiny Clause Normal Forms
- PRocH: Proof Reconstruction for HOL Light
- Reducibility among Combinatorial Problems
- Ribbon Proofs for Separation Logic
- Encoding Monomorphic and Polymorphic Types
- MaSh: Machine Learning for Sledgehammer
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
- A Machine-Oriented Logic Based on the Resolution Principle
- Fast LCF-Style Proof Reconstruction for Z3
- Sledgehammer: Judgement Day
