×

DAG sequent proofs with a substitution rule. (English) Zbl 1279.03079

Artemov, Sergei (ed.) et al., We will show them! Essays in honour of Dov Gabbay on his 60th birthday. Volume 1. London: College Publications (ISBN 1-904987-11-7/pbk; 1-904987-25-7/hbk). Tributes 1, 671-686 (2005).
From the introduction: In this paper, we investigate a sequent proof method known to have short proofs even for the hardest known propositional formulas. We explore some of the proof-theoretical properties of this inference system and investigate how it can be transformed in a tableau-like decision procedure.
For the entire collection see [Zbl 1202.03006].

MSC:

03F07 Structure of proofs
03B05 Classical propositional logic
PDFBibTeX XMLCite