Logical Approaches to Computational Barriers

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 |