FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Tableaux Calculus for Reducing Proof Size

Authors: Michael Peter Lettmann and Nicolas Peltier

Paper Information

Title:A Tableaux Calculus for Reducing Proof Size
Authors:Michael Peter Lettmann and Nicolas Peltier
Proceedings:IJCAR Proceedings 9th IJCAR, 2018
Editors: Stephan Schulz, Didier Galmiche and Roberto Sebastiani
Keywords:Proof theory, First-order logic, Tableau calculus, Proof compression
Abstract:

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.

Pages:16
Talk:Jul 15 10:00 (Session 101D: Logics and Calculi)
Paper: