Implementing the clausal normal form transformation with proof generation
Hans de Nivelle, Boris Yur'evich Konev, Renate A. Schmidt · 2003
Abstract. We explain how we intend to implement the clausal normal form transformation with proof generation. We present a convenient data structure for sequent calculus proofs, which will be used for representing the generated proofs. The data structure allows easy proof checking and generation of proofs. In addition, it allows convenient implementation of proof normalization, which is necessary in order to keep the size of the generated proofs acceptable. 1