Pym, D;
Ritter, E;
Robinson, E;
(2014)
A proof-theoretic analysis of the classical propositional matrix method.
Journal of Logic and Computation
, 24
(1)
283 - 301.
10.1093/logcom/exs045.
PDF
PymRitterRobinson.pdf Download (345kB) |
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. © 2012 The Author, 2012. Published by Oxford University Press.
Type: | Article |
---|---|
Title: | A proof-theoretic analysis of the classical propositional matrix method |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1093/logcom/exs045 |
Publisher version: | http://dx.doi.org/10.1093/logcom/exs045 |
Additional information: | Authors may upload their accepted manuscript PDF to an institutional and/or centrally organized repository, provided that public availability is delayed until 12 months after first online publication in the journal. This is a pre-copyedited, author-produced PDF of an article accepted for publication in Journal of Logic and Computation following peer review. The version of record 'Pym, D; Ritter, E; Robinson, E; (2014) A proof-theoretic analysis of the classical propositional matrix method. Journal of Logic and Computation, 24 (1) 283 - 301. 10.1093/logcom/exs045' is available online at: http://dx.doi.org/10.1093/logcom/exs045 |
Keywords: | Classical logic, Propositional logic, Proof theory, Category theory, Matrix method |
UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
URI: | https://discovery.ucl.ac.uk/id/eprint/1464199 |
Archive Staff Only
View Item |