FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Partial Regularization of First-Order Resolution Proofs

Authors: Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo

Paper Information

Title:Partial Regularization of First-Order Resolution Proofs
Authors:Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo
Proceedings:UITP Full Papers
Editors: Mateja Jamnik and Christoph Lüth
Keywords:proof compression, first-order logic, resolution, unification
Abstract:

ABSTRACT. Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression techniques. There are fewer techniques for compressing first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. One method for propositional proof compression is partial regularization, which removes an inference n when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from n to the root of the proof. This paper describes the generalization of the partial-regularization algorithm RecyclePivotsWithIntersection [10] from propositional logic to first-order logic. An empirical evaluation of the generalized algorithm and its combinations with the previously lifted GreedyLinearFirstOrderLowerUnits algorithm [12] is also presented.

Pages:12
Talk:Jul 13 11:00 (Session 86N: UITP 2)
Paper: