Skip to Main content Skip to Navigation
Conference papers

A Tableaux Calculus for Reducing Proof Size

Michael Lettmann Nicolas Peltier 1
1 CAPP - Calculs algorithmes programmes et preuves
LIG - Laboratoire d'Informatique de Grenoble [2007-2015]
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 can reduce the size of the proof. It is shown that the obtained proof procedure is sound, refutationally complete and can reduce the size of the tableau by an exponential factor. The approach is compatible with all usual refinements of tableaux.
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download
Contributor : Nicolas Peltier <>
Submitted on : Tuesday, November 5, 2019 - 9:58:23 AM
Last modification on : Thursday, July 9, 2020 - 9:44:45 AM
Document(s) archivé(s) le : Thursday, February 6, 2020 - 9:28:32 PM


Files produced by the author(s)


  • HAL Id : hal-01946472, version 1



Michael Lettmann, Nicolas Peltier. A Tableaux Calculus for Reducing Proof Size. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, 2018, Oxford, United Kingdom. ⟨hal-01946472⟩



Record views


Files downloads