Semi-intelligible Isar proofs from machine-generated proofs
From MaRDI portal
(Redirected from Publication:287340)
Recommendations
Cites work
- scientific article; zbMATH DE number 1614711 (Why is no real title available?)
- scientific article; zbMATH DE number 1614717 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 3871342 (Why is no real title available?)
- scientific article; zbMATH DE number 48878 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Analytical meets numerical relativity: status of complete gravitational waveform models for binary black holes
- Assertion-level proof representation with under-specification
- Automated analysis of regular algebra
- Computing Tiny Clause Normal Forms
- Concrete semantics. With Isabelle/HOL
- Encoding monomorphic and polymorphic types
- Equational reasoning in Isabelle
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Improving legibility of natural deduction proofs is not trivial
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Lightweight relevance filtering for machine-generated resolution problems
- MaSh: machine learning for Sledgehammer
- Methods of lemma extraction in natural deduction proofs
- More SPASS with Isabelle
- Obvious inferences
- On the rules of suppositions in formal logic
- PRocH: proof reconstruction for HOL Light
- Property-directed incremental invariant generation
- Reducibility among combinatorial problems
- Resolution theorem proving
- Ribbon proofs for separation logic
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- SMT proof checking using a logical framework
- Satallax: An Automatic Higher-Order Prover
- Sledgehammer: judgement day
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- System description: E 1.8
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Translating higher-order clauses to first-order clauses
- Untersuchungen über das logische Schliessen. I
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
Cited in
(21)- A formal proof of the expressiveness of deep learning
- A formal proof of the expressiveness of deep learning
- Mining the Archive of Formal Proofs
- A verified SAT solver framework with learn, forget, restart, and incrementality
- CoSMed: a confidentiality-verified social media platform
- A verified SAT solver framework with learn, forget, restart, and incrementality
- An Isabelle proof method language
- A proof strategy language and proof script generation for Isabelle/HOL
- Mechanizing the metatheory of Sledgehammer
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Automatic proof and disproof in Isabelle/HOL
- Theorem proving as constraint solving with coherent logic
- Goal-oriented conjecturing for Isabelle/HOL
- Scalable fine-grained proofs for formula processing
- A learning-based fact selector for Isabelle/HOL
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Hammer for Coq: automation for dependent type theory
- Mining state-based models from proof corpora
- Proofs and reconstructions
- VizAR: visualization of automated reasoning proofs (system description)
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
Describes a project that uses
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)
