Tech Reports

ULCS-02-008

TPI-Disputes and Proof by Clausal Tableaux

Paul E. Dunne


Abstract

Two--Party Immediate Response Disputes (tpi-disputes) are a dialogue game formalism providing a sound and complete proof scheme for credulous reasoning in argument systems. In earlier work it has been shown that this dialogue protocol can be interpreted as a proof calculus with which to establish unsatisfiability of propositional formula presented in cnf, and that viewed thus, the number of 'moves' taken to resolve a dispute -- i.e. prove that $Phi$ is unsatisfiable -- is bounded below by the number of lines in the shortest derivation of $Rightarrow egPhi$ in a cut-free Gentzen System. In this note we prove an upper bound on the number of moves needed, showing this to be of the same order as the size of the smallest clausal tableau refutation of $Phi$. It thereby follows that tpi-disputes are 'polynomially equivalent' to these proof systems.

Keywords: Argument System, Credulous Acceptance, Dialogue Game, Tableau Proof.

[Full Paper]