Data compression for proof replay

DOI10.1007/s10817-008-9109-2zbMath1191.68616OpenAlexW1987719146MaRDI QIDQ1040776

Hasan Amjad

Publication date: 25 November 2009

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

Full work available at URL: https://doi.org/10.1007/s10817-008-9109-2

zbMATH Keywords

SAT solversinteractive theorem provingproof translation

Mathematics Subject Classification ID

Related Items

Resolution proof transformation for compression and interpolation ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL

Uses Software

• Coq
• Isabelle
• MiniSat
• ML
• PVS
• MetaPRL
• HOL
• HOL Light
• Chaff
• CBMC
• PATRICIA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficiently checking propositional refutations in HOL theorem provers
• Isabelle. A generic theorem prover
• On-line construction of compact directed acyclic word graphs
• On-line construction of suffix trees
• Fast Algorithms for Finding Nearest Common Ancestors
• Resolution Is Not Automatizable Unless W[P Is Tractable]
• Algorithms on Strings, Trees and Sequences
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• A machine program for theorem-proving
• Tools and Algorithms for the Construction and Analysis of Systems