A proof-theoretic analysis of the classical propositional matrix method

David Pym; Eike Ritter; Edmund Robinson

doi:10.1093/logcom/exs045

A proof-theoretic analysis of the classical propositional matrix method

David Pym, Eike Ritter, Edmund Robinson

Computing Science

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	283-301
Number of pages	19
Journal	Journal of Logic and Computation
Volume	24
Issue number	1
Early online date	21 Nov 2012
DOIs	https://doi.org/10.1093/logcom/exs045
Publication status	Published - Feb 2014

Keywords

classical logic
propositional logic
proof theory
category theory
matrix method

Access to Document

10.1093/logcom/exs045

Cite this

@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 = feb,

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

SN - 0955-792X

VL - 24

SP - 283

EP - 301

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 1

ER -

A proof-theoretic analysis of the classical propositional matrix method

Abstract

Keywords

Access to Document

Fingerprint

Cite this