Scalable fine-grained proofs for formula processing

DOI10.1007/S10817-018-09502-YzbMath1468.68278OpenAlexW2906782500WikidataQ113901244 ScholiaQ113901244MaRDI QIDQ5919479

Jasmin Christian Blanchette, Mathias Fleury, Haniel Barbosa, Pascal Fontaine

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-02515103/file/processing_article.pdf

zbMATH Keywords

rewritingSMTproof checkingformula processingproof productionproof reconstruction

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Unnamed Item ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SMT-LIB
• SPASS
• Metis_
• z3
• HOL
• HOL Light
• veriT
• CVC Lite
• E Theorem Prover
• Easychair
• TRAMP
• GAPT
• Psyche

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semi-intelligible Isar proofs from machine-generated proofs
• A higher-order implementation of rewriting
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Translation of resolution proofs into short first-order proofs without choice axioms
• System Description: GAPT 2.0
• Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture
• Understanding Resolution Proofs through Herbrand’s Theorem
• System Description: E 1.8
• The TPTP Typed First-Order Form with Arithmetic
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• Congruence Closure with Free Variables
• Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A framework for defining logics
• Exploiting Symmetry in SMT Problems
• A system of interaction and structure
• The challenge of computer mathematics
• Rocket-Fast Proof Checking for SMT Solvers
• Proof Checking and Logic Programming
• Fast LCF-Style Proof Reconstruction for Z3
• Tools and Algorithms for the Construction and Analysis of Systems
• Scalable fine-grained proofs for formula processing

This page was built for publication: Scalable fine-grained proofs for formula processing