On the Length of Medial-Switch-Mix Derivations
| Autor: | Lutz Straßburger, Paola Bruscoli |
|---|---|
| Přispěvatelé: | University of Bath [Bath], Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Kennedy, Juliet, de Queiroz, Ruy J.G.B., Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Discrete mathematics
Proof complexity Logic Modulo [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 0102 computer and information sciences 02 engineering and technology 01 natural sciences Theoretical Computer Science Quadratic equation Proof calculus Computational Theory and Mathematics 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Rule of inference Commutative property Associative property Deep Inference proof complexity switch-medial term rewritng Deep inference Mathematics |
| Zdroj: | WoLLIC 2017-Logic, Language, Information, and Computation WoLLIC 2017-Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom Bruscoli, P & Strassburger, L 2017, On the Length of Medial-Switch-Mix Derivations . in J Kennedy & R J G B de Queiroz (eds), Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017 : Proceedings . Lecture Notes in Computer Science, vol. 10388, Springer Verlag, Berlin, Germany, pp. 68-79 . https://doi.org/10.1007/978-3-662-55386-2_5 Logic, Language, Information, and Computation ISBN: 9783662553855 WoLLIC |
| Popis: | International audience; 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 con-nectives 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|