A Tableaux Calculus for Reducing Proof Size

TL;DR

This paper introduces a tableau calculus that compresses clause representations by merging similar literals, significantly reducing proof sizes while maintaining soundness and completeness.

Contribution

It presents a novel tableau calculus that merges similar literals to exponentially decrease proof size, compatible with existing tableau refinements.

Findings

Proof size reduced exponentially.

The calculus is sound and refutationally complete.

Compatible with standard tableau refinements.

Abstract

A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are fused when possible, which reduces the size of the proof. It is shown that the obtained proof procedure is sound, refutationally complete and allows to reduce the size of the tableau by an exponential factor. The approach is compatible with all usual refinements of tableaux.