TY - JOUR
T1 - Towards the compression of first-order resolution proofs by lowering unit clauses
AU - Gorzny, Jan
AU - Paleo, Bruno Woltzenlogel
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - The recently developed LowerUnits algorithm compresses propositional resolution proofs generated by SAT- and SMT-solvers by postponing and lowering resolution inferences involving unit clauses, which have exactly one literal. This paper describes a generalization of this algorithm to the case of first-order resolution proofs generated by automated theorem provers. An empirical evaluation of a simplified version of this algorithm on hundreds of proofs shows promising results.
AB - The recently developed LowerUnits algorithm compresses propositional resolution proofs generated by SAT- and SMT-solvers by postponing and lowering resolution inferences involving unit clauses, which have exactly one literal. This paper describes a generalization of this algorithm to the case of first-order resolution proofs generated by automated theorem provers. An empirical evaluation of a simplified version of this algorithm on hundreds of proofs shows promising results.
UR - http://www.scopus.com/inward/record.url?scp=84984650544&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-21401-6_24
DO - 10.1007/978-3-319-21401-6_24
M3 - Conference article
SN - 0302-9743
VL - 9195
SP - 356
EP - 366
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - 25th International Conference on Automated Deduction CADE 2015
Y2 - 1 August 2015 through 7 August 2015
ER -