Towards the compression of first-order resolution proofs by lowering unit clauses

Jan Gorzny; Bruno Woltzenlogel Paleo

doi:10.1007/978-3-319-21401-6_24

Towards the compression of first-order resolution proofs by lowering unit clauses

Jan Gorzny^*
, Bruno Woltzenlogel Paleo

^*Corresponding author for this work

Research output: Contribution to journal › Conference article › peer-review

5 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	356-366
Number of pages	11
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9195
DOIs	https://doi.org/10.1007/978-3-319-21401-6_24
Publication status	Published - 2015
Externally published	Yes
Event	25th International Conference on Automated Deduction CADE 2015 - Berlin, Germany Duration: 1 Aug 2015 → 7 Aug 2015

Access to Document

10.1007/978-3-319-21401-6_24

Cite this

@article{07798ebd63d04e7cb9f99007a3780eeb,

title = "Towards the compression of first-order resolution proofs by lowering unit clauses",

abstract = "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.",

author = "Jan Gorzny and Paleo, \{Bruno Woltzenlogel\}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 25th International Conference on Automated Deduction CADE 2015 ; Conference date: 01-08-2015 Through 07-08-2015",

year = "2015",

doi = "10.1007/978-3-319-21401-6\_24",

language = "English",

volume = "9195",

pages = "356--366",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

Towards the compression of first-order resolution proofs by lowering unit clauses. / Gorzny, Jan; Paleo, Bruno Woltzenlogel.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 9195, 2015, p. 356-366.

Research output: Contribution to journal › Conference article › peer-review

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 - https://www.scopus.com/pages/publications/84984650544

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 -

Towards the compression of first-order resolution proofs by lowering unit clauses

Abstract

Access to Document

Other files and links

Fingerprint

Cite this