Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Using Tables to Construct Non-Redundant Proofs

Speaker: Vivek Nigam
Slot: Array, 11:40-12:00, col. 2


Proofs containing more than one subproof for a common subgoal are less preferred
in frameworks such as Proof Carrying Code, where proofs are stored and
communicated, than proofs that don't contain such redundancies. In this
paper, we show how (cut-free) proofs can be transformed into non-redundant
cut-proofs. Two main questions arise when trying to construct these
non-redundant proofs: First, which cut-formulas should be used; Second, where to
perform cut rules. Some advances in proof theory, namely, our better
understanding of focused proofs, allows us to propose the following answers: We
use only atomic subgoals of the original proof; and we place cut rules only at
the end of the \emph{asynchronous phases}. The backbone of a non-redundant proof
is a tree, called \emph{tree of multicut derivations} ($\tmcd$), where a node is
a derivation containing only multicut rules, and an edge represents the
provability dependency between a subgoal introduced by a node's multicut
rule and another (tree of) multicut derivation. We show how to obtain a $\tmcd$
from an existing proof.

websites: Arnold Beckmann 2008-05-19