A proof-theoretic analysis of the classical propositional matrix method

David Pym, Eike Ritter, Edmund Robinson

Research output: Contribution to journalArticle

Abstract

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.
Original languageEnglish
Pages (from-to)283-301
Number of pages19
JournalJournal of Logic and Computation
Volume24
Issue number1
Early online date21 Nov 2012
DOIs
Publication statusPublished - Feb 2014

    Fingerprint

Keywords

  • classical logic
  • propositional logic
  • proof theory
  • category theory
  • matrix method

Cite this