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: |