Data compression for proof replay
type: Item
instance of: scholarly article
title: Data compression for proof replay
zbMATH Open document ID: 1191.68616
author: Hasan Amjad
published in: Journal of Automated Reasoning
publication date: 2009-11-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5638511
zbMATH Keywords: proof translation
zbMATH Keywords: SAT solvers
zbMATH Keywords: interactive theorem proving
describes a project that uses: Isabelle
describes a project that uses: MetaPRL
describes a project that uses: CBMC
describes a project that uses: Coq
describes a project that uses: ML
describes a project that uses: MiniSat
describes a project that uses: PVS
describes a project that uses: HOL
describes a project that uses: HOL Light
describes a project that uses: Chaff
describes a project that uses: PATRICIA
MaRDI profile type: Publication
full work available at URL: s10817-008-9109-2
OpenAlex ID: W1987719146
cites work: Resolution Is Not Automatizable Unless W[P] Is Tractable
cites work: Q4804887
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Introduction to algorithms
cites work: A machine program for theorem-proving
cites work: Q5315023
cites work: Theory and Applications of Satisfiability Testing
cites work: Q5287513
cites work: Algorithms on Strings, Trees and Sequences
cites work: Fast Algorithms for Finding Nearest Common Ancestors
cites work: On-line construction of compact directed acyclic word graphs
cites work: Q3396552
cites work: Isabelle. A generic theorem prover
cites work: Q4790648
cites work: On-line construction of suffix trees
cites work: Efficiently checking propositional refutations in HOL theorem provers
DOI: 10.1007/S10817-008-9109-2
description: scientific article; zbMATH DE number 5638511