A proof-theoretic analysis of the classical propositional matrix method
David J. Pym, Eike Ritter, E. Powell Robinson · Journal of Logic and Computation · 2012
The matrix method, due to Bibel and Andrews, is a proof procedure designed for automated theorem-proving. We show that underlying this method is a fully structured combinatorial model of conventional classical proof theory.