Output details

A proof-theoretic analysis of the classical propositional matrix method

<11>This paper uses the outcomes of the EPSRC-funded project `The Semantic of Classical Proofs', which solved the long-standing open problem of giving a non-trivial categorical semantics to properly symmetric classical sequent-calculus proofs, to establish perhaps the first non-trivial connection between efficiency-motivated theorem-proving procedures (here, the somewhat geometric matrix method) and proof-theoretic semantics. Published in the leading journal for logic and its applications in computing, it has opened up a line of research connecting game semantics, geometry, proof theory, and (automated) theorem proving at level of mathematical depth not previously reached.