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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.