English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Resolution and superposition are common techniques which have seen widespreaduse with propositional and first-order logic in modern theorem provers. Inthese cases, resolution proof production is a key feature of such tools;however, the proofs that they produce are not necessarily as concise aspossible. For propositional resolution proofs, there are a wide variety ofproof compression techniques. There are fewer techniques for compressingfirst-order resolution proofs generated by automated theorem provers. Thispaper describes an approach to compressing first-order logic proofs based onlifting proof compression ideas used in propositional logic to first-orderlogic. One method for propositional proof compression is partialregularization, which removes an inference $\eta$ when it is redundant in thesense that its pivot literal already occurs as the pivot of another inferencein every path from $\eta$ to the root of the proof. This paper describes thegeneralization of the partial-regularization algorithmRecyclePivotsWithIntersection [10] from propositional logic to first-orderlogic. The generalized algorithm performs partial regularization of resolutionproofs containing resolution and factoring inferences with unification. Anempirical evaluation of the generalized algorithm and its combinations with thepreviously lifted GreedyLinearFirstOrderLowerUnits algorithm [12] is alsopresented

Partial Regularization of First-Order Resolution Proofs