 |
Grenoble Informatics Laboratory |  |
Conference papers
A Tableaux Calculus for Reducing Proof Size
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.
Cited literature [15 references]
https://hal.archives-ouvertes.fr/hal-01946472
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
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
File
paper_12.pdf
Files produced by the author(s)
