Can I read Partial Regularization of First-Order Resolution Proofs on EtoBox?

Partial Regularization of First-Order Resolution Proofs by Gorzny, Jan; Postan, Ezequiel; Paleo, Bruno Woltzenlogel is a scholarly article available to read on EtoBox.

What is Partial Regularization of First-Order Resolution Proofs about?

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 $\eta$ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta$ 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. The generalized algorithm performs partial regularization of resolution proofs containing re

Author

Gorzny, Jan; Postan, Ezequiel; Paleo, Bruno Woltzenlogel

Published

2018

Language

EN