Projects per year
Abstract
Switch and medial are two inference rules that play a central role in many deep inference proof systems. In specific proof systems, the mix rule may also be present. In this paper we show that the maximal length of a derivation using only the inference rules for switch, medial, and mix, modulo associativity and commutativity of the two binary connectives involved, is quadratic in the size of the formula at the conclusion of the derivation. This shows, at the same time, the termination of the rewrite system.
Original language | English |
---|---|
Title of host publication | Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017 |
Subtitle of host publication | Proceedings |
Editors | Juliet Kennedy, Ruy J.G.B. de Queiroz |
Place of Publication | Berlin, Germany |
Publisher | Springer Verlag |
Pages | 68-79 |
ISBN (Electronic) | 9783662553862 |
ISBN (Print) | 9783662553855 |
DOIs | |
Publication status | Published - Jun 2017 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 10388 |
Keywords
- Deep Inference, proof complexity, switch-medial, term rewritng
ASJC Scopus subject areas
- Computational Theory and Mathematics
- Logic
- Theoretical Computer Science
Fingerprint
Dive into the research topics of 'On the Length of Medial-Switch-Mix Derivations'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Efficient and Natural Proof Systems
Guglielmi, A. (PI), Bruscoli, P. (CoI) & McCusker, G. (CoI)
Engineering and Physical Sciences Research Council
1/02/13 → 12/05/16
Project: Research council