A proof-theoretic analysis of the classical propositional matrix method

David Pym, Eike Ritter, Edmund Robinson

Research output: Contribution to journalArticlepeer-review

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
DOIs
Publication statusPublished - 1 Feb 2014

Keywords

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

ASJC Scopus subject areas

  • Logic
  • Theoretical Computer Science
  • Software
  • Hardware and Architecture
  • Arts and Humanities (miscellaneous)

Fingerprint

Dive into the research topics of 'A proof-theoretic analysis of the classical propositional matrix method'. Together they form a unique fingerprint.

Cite this