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

Computer 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
DOIs	https://doi.org/10.1093/logcom/exs045
Publication status	Published - 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)

Access to Document

10.1093/logcom/exs045

Cite this

@article{55f27c752a824278bd1502a2e49697dc,

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 = "category theory, Classical logic, matrix method, proof theory, propositional logic",

author = "David Pym and Eike Ritter and Edmund Robinson",

year = "2014",

month = feb,

day = "1",

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/1

Y1 - 2014/2/1

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 - category theory

KW - Classical logic

KW - matrix method

KW - proof theory

KW - propositional logic

UR - http://www.scopus.com/inward/record.url?scp=84892696758&partnerID=8YFLogxK

U2 - 10.1093/logcom/exs045

DO - 10.1093/logcom/exs045

M3 - Article

AN - SCOPUS:84892696758

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

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this