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

Automated Theorem Proving
Theorem proving
Proof Theory
Matrix Method
Model
Conventional

Keywords

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

Cite this

A proof-theoretic analysis of the classical propositional matrix method. / Pym, David; Ritter, Eike; Robinson, Edmund.

In: Journal of Logic and Computation, Vol. 24, No. 1, 02.2014, p. 283-301.

Research output: Contribution to journalArticle

Pym, David ; Ritter, Eike ; Robinson, Edmund. / A proof-theoretic analysis of the classical propositional matrix method. In: Journal of Logic and Computation. 2014 ; Vol. 24, No. 1. pp. 283-301.
@article{63a00fe4c18a47b7ac88e785c7915805,
title = "A proof-theoretic analysis of the classical propositional matrix method",
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.",
keywords = "classical logic, propositional logic, proof theory, category theory, matrix method",
author = "David Pym and Eike Ritter and Edmund Robinson",
year = "2014",
month = "2",
doi = "10.1093/logcom/exs045",
language = "English",
volume = "24",
pages = "283--301",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "1",

}

TY - JOUR

T1 - A proof-theoretic analysis of the classical propositional matrix method

AU - Pym, David

AU - Ritter, Eike

AU - Robinson, Edmund

PY - 2014/2

Y1 - 2014/2

N2 - 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.

AB - 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.

KW - classical logic

KW - propositional logic

KW - proof theory

KW - category theory

KW - matrix method

U2 - 10.1093/logcom/exs045

DO - 10.1093/logcom/exs045

M3 - Article

VL - 24

SP - 283

EP - 301

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 1

ER -