Reliable reconstruction of fine-grained proofs in a proof assistant
From MaRDI portal
Publication:2055877
DOI10.1007/978-3-030-79876-5_26OpenAlexW3180619128MaRDI QIDQ2055877
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_26
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (4)
Quantifier simplification by unification in SMT ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Theorem proving as constraint solving with coherent logic ⋮ Flexible proof production in an industrial-strength SMT solver
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Semi-intelligible Isar proofs from machine-generated proofs
- Lightweight relevance filtering for machine-generated resolution problems
- Edinburgh LCF. A mechanized logic of computation
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Extending SMT solvers to higher-order logic
- An Isabelle/HOL formalisation of Green's theorem
- Revisiting enumerative instantiation
- SMT proof checking using a logical framework
- An Isabelle/HOL Formalisation of Green’s Theorem
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Satisfiability Modulo Theories
- Congruence Closure with Free Variables
- Extending Sledgehammer with SMT Solvers
- MaSh: Machine Learning for Sledgehammer
- Fast LCF-Style Proof Reconstruction for Z3
- Sledgehammer: Judgement Day
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Scalable fine-grained proofs for formula processing
This page was built for publication: Reliable reconstruction of fine-grained proofs in a proof assistant
