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 journalConference articlepeer-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 languageEnglish
Pages (from-to)356-366
Number of pages11
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9195
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event25th International Conference on Automated Deduction CADE 2015 - Berlin, Germany
Duration: 1 Aug 20157 Aug 2015

Fingerprint

Dive into the research topics of 'Towards the compression of first-order resolution proofs by lowering unit clauses'. Together they form a unique fingerprint.

Cite this