author = {Martin Giese},
title = {{Saturation up to Redundancy for Tableau and Sequent Calculi}},
booktitle = {{Logic for Programming, Artificial Intelligence, and Reasoning, 13th Intl. Conf., LPAR 2006, Phnom Penh, Cambodia}},
language = {english},
abstract = {We discuss an adaptation of the technique of saturation up to redundancy, as introduced by Bachmair and Ganzinger, to tableau and sequent calculi for classical first-order logic. This technique can be used to easily show the completeness of optimized calculi that contain destructive rules e.g. for simplification, rewriting with equalities, etc., which is not easily done with a standard Hintikka-style completeness proof. The notions are first introduced for Smullyan-style ground tableaux, and then extended to constrained formula free-variable tableaux.},
series = {LNCS},
volume = {4246},
pages = {182--196},
publisher = {Springer},
isbn_issn = {3540482814},
year = {2006},
editor = {Miki Hermann and Andrei Voronkov},
refereed = {yes},
length = {15},
conferencename = {LPAR06}