A proof-theoretic analysis of the classical propositional matrix method

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

External organisations

  • University of Aberdeen
  • Queen Mary University of London

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.

Details

Original languageEnglish
Pages (from-to)283-301
Number of pages19
JournalJournal of Logic and Computation
Volume24
Issue number1
Publication statusPublished - 1 Feb 2014

Keywords

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