Partial Regularization of First-Order Resolution Proofs

EasyChair Preprint 360

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.

Keyphrases: Proof Compression, first-order logic, resolution, unification

@booklet{EasyChair:360,
  author    = {Jan Gorzny and Ezequiel Postan and Bruno Woltzenlogel Paleo},
  title     = {Partial Regularization of First-Order Resolution Proofs},
  doi       = {10.29007/r4rm},
  howpublished = {EasyChair Preprint 360},
  year      = {EasyChair, 2018}}