A Tableaux Calculus for Reducing Proof Size
Logic in Computer Science
2018-01-15 v1
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.
Keywords
Cite
@article{arxiv.1801.04163,
title = {A Tableaux Calculus for Reducing Proof Size},
author = {Michael Peter Lettmann and Nicolas Peltier},
journal= {arXiv preprint arXiv:1801.04163},
year = {2018}
}
Comments
Technical Report