On the proof complexity of deep inference

ABSTRACT

We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.

REFERENCES

• 1: Brünnler, K. 2003a. Atomic cut elimination for classical logic. In Proceedings of the International Workshop on Computer Logic (CSL'03), M. Baaz and J. A. Makowsky, Eds. Lecture Notes in Computer Science, vol. 2803. Springer, 86--97. http://www.iam.unibe.ch/kai/Papers/ace.pdf.
• 2: Brünnler, K. 2003b. Two restrictions on contraction. Logic J. IGPL 11, 5, 525--529. http://www.iam.unibe.ch/~kai/Papers/RestContr.pdf.
• 3: Brünnler, K. 2004. Deep Inference and Symmetry in Classical Proofs. Logos, Berlin. http://www.iam.unibe.ch/~kai/Papers/phd.pdf.
• 4: Brünnler, K. 2006a. Cut elimination inside a deep inference system for classical predicate logic. Studia Logica 82, 1, 51--71. http://www.iam.unibe.ch/kai/Papers/q.pdf.
• 5: Brünnler, K. 2006b. Deep inference and its normal form of derivations. In Computability in Europe 2006, A. Beckmann et al., Eds. Lecture Notes in Computer Science, vol. 3988. Springer, 65--74. http://www.iam.unibe.ch/~kai/Papers/n.pdf.
• 6: Brünnler, K. 2006c. Deep sequent systems for modal logic. In Advances in Modal Logic, G. Governatori et al., Eds. Vol. 6. College Publications, 107--119. http://www.aiml.net/volumes/volume6/Bruennler.ps.
• 7: Brünnler, K. 2006d. Locality for classical logic. Notre Dame J. Formal Logic 47, 4, 557--580. http://www.iam.unibe.ch/~kai/Papers/LocalityClassical.pdf.
• 8: Brünnler, K. and Guglielmi, A. 2004. A first order system with finite choice of premises. In First-Order Logic Revisited, V. Hendricks et al., Eds. Logische Philosophie. Logos, 59--74. http://www.iam.unibe.ch/~kai/Papers/FinitaryFOL.pdf.
• 9: Brünnler, K. and Lengrand, S. 2005. On two forms of bureaucracy in derivations. In Proceedings of the International Collequium on Automata Languages and Programming, Structures and Deduction (ICALP), P. Bruscoli et al., Eds. Technische Universität Dresden, 69--80. ISSN 1430-211X. http://www.iam.unibe.ch/~kai/Papers/sd05.pdf.
• 10: Kai Brünnler , Alwen Fernanto Tiu, A Local System for Classical Logic, Proceedings of the Artificial Intelligence on Logic for Programming, p.347-361, December 03-07, 2001
• 11: Paola Bruscoli, A Purely Logical Account of Sequentiality in Proof Search, Proceedings of the 18th International Conference on Logic Programming, p.302-316, July 29-August 01, 2002
• 12: Bruscoli, P. and Guglielmi, A. 2007. On analytic inference rules in the calculus of structures. http://cs.bath.ac.uk/ag/p/Onan.pdf.
• 13: Buss, S. R. 1987. Polynomial size proofs of the propositional pigeonhole principle. J. Symbolic Logic 52, 4, 916--927.
• 14: Clote, P. and Kranakis, E. 2002. Boolean Functions and Computation Models. Springer.
• 15: Stephen Cook , Robert Reckhow, On the lengths of proofs in the propositional calculus (Preliminary Version), Proceedings of the sixth annual ACM symposium on Theory of computing, p.135-148, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803893]
• 16: Cook, S. A. and Reckhow, R. A. 1979. The relative efficiency of propositional proof systems. J. Symbolic Logic 44, 1, 36--50.
• 17: Di Gianantonio, P. 2004. Structures for multiplicative cyclic linear logic: Deepness vs cyclicity. In Proceedings of the International Workshop on Computer Science Logic (CSL'04), J. Marcinkowski and A. Tarlecki, Eds. Lecture Notes in Computer Science, vol. 3210. Springer-Verlag, 130--144. http://www.dimi.uniud.it/~pietro/papers/Soft-copy-ps/scll.ps.gz.
• 18: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 19: Rajeev Goré , Alwen Tiu, Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for S5, Journal of Logic and Computation, v.17 n.4, p.767-794, August 2007 [doi>10.1093/logcom/exm026]
• 20: Guglielmi, A. 2003. Resolution in the calculus of structures. http://cs.bath.ac.uk/ag/p/AG10.pdf.
• 21: Guglielmi, A. 2004. Formalism B. http://cs.bath.ac.uk/ag/p/AG13.pdf.
• 22: Guglielmi, A. 2005. The problem of bureaucracy and identity of proofs from the perspective of deep inference. In Structures and Deduction Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP), P. Bruscoli et al., Eds. Technische Universität Dresden, 53--68. ICALP Workshop. ISSN 1430-211X. http://cs.bath.ac.uk/ag/p/AG14.pdf.
• 23: Guglielmi, A. 2007a. On the proof complexity of deep inference—Conjecture. Prolog program. http://cs.bath.ac.uk/ag/p/PrComplDI.plg.
• 24: Alessio Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic (TOCL), v.8 n.1, p.1-es, January 2007 [doi>10.1145/1182613.1182614]
• 25: Guglielmi, A. and Gundersen, T. 2008. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science 4, 1--9, 1--36.
• 26: Alessio Guglielmi , Lutz Straßburger, Non-commutativity and MELL in the Calculus of Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.54-68, September 10-13, 2001
• 27: Alessio Guglielmi , Lutz Straßburger, A Non-commutative Extension of MELL, Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, p.231-246, October 14-18, 2002
• 28: Guglielmi, A. and Straßburger, L. 2007. A system of interaction and structure IV: The exponentials. In the second round of revision for Mathematical Structures in Computer Science. http://www.lix.polytechnique.fr/~lutz/papers/NELbig.pdf.
• 29: Guiraud, Y. 2006. The three dimensions of proofs. Ann. Pure Appl. Logic 141, 1-2, 266--295. http://www.loria.fr/~guiraudy/recherche/cos1.pdf.
• 30: Japaridze, G. 2008. Cirquent calculus deepened. J. Logic Comput. 18, 6, 983--1028.
• 31: Kahramanoğullari, O. 2006a. Nondeterminism and language design in deep inference. Ph.D. thesis, Technische Universität Dresden. http://www.doc.ic.ac.uk/~ozank/Papers/ozansthesis.pdf.
• 32: Kahramanoğullari, O. 2006b. Reducing nondeterminism in the calculus of structures. In Proceedings of the International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR), M. Hermann and A. Voronkov, Eds. Lecture Notes in Artificial Intelligence, vol. 4246. Springer-Verlag, 272--286. http://www.doc.ic.ac.uk/~ozank/Papers/reducingNondet.pdf.
• 33: Kahramanoğullari, O. 2007a. Maude as a platform for designing and implementing deep inference systems. In Proceedings of the 8th International Workshop on Rule-Based Programming. Electronic Notes in Theoretical Computer Science. Elsevier. In press. http://www.doc.ic.ac.uk/~ozank/Papers/rule07.pdf.
• 34: Kahramanoğullari, O. 2007b. System BV is NP-complete. Ann. Pure Appl. Logic 152, 1--3, 107--121.
• 35: Krajíček, J. and Pudlák, P. 1989. Propositional proof systems, the consistency of first order theories and the complexity of computations. J. Symbolic Logic 54, 3, 1063--1079.
• 36: Francois Lamarche , Lutz Strassburger, Constructing Free Boolean Categories, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.209--218, June 26-29, 2005 [doi>10.1109/LICS.2005.13]
• 37: Lamarche, F. and Straßburger, L. 2005b. Naming proofs in classical propositional logic. In Typed Lambda Calculi and Applications, P. Urzyczyn, Ed. Lecture Notes Computer Science, vol. 3461. Springer, 246--261. http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL. pdf.
• 38: Lamarche, F. and Straßburger, L. 2006. From proof nets to the free *-autonomous category. Logical Methods Comput. Sci. 2, 4, 3:1--44. http://arxiv.org/pdf/cs.L0/0605054.
• 39: Robert Allen Reckhow, On the lengths of proofs in the propositional calculus., 1976
• 40: Statman, R. 1978. Bounds for proof-search and speed-up in the predicate calculus. Ann. Math. Logic 15, 225--287.
• 41: Stouppa, P. 2007. A deep inference system for the modal logic S5. Studia Logica 85, 2, 199--214. http://www.iam.unibe.ch/til/publications/pubitems/pdfs/sto07.pdf.
• 42: Lutz Straßburger, A Local System for Linear Logic, Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, p.388-402, October 14-18, 2002
• 43: Straßburger, L. 2003a. Linear logic and noncommutativity in the calculus of structures. Ph.D. thesis, Technische Universität Dresden. http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf.
• 44: Lutz Straßburger, MELL in the calculus of structures, Theoretical Computer Science, v.309 n.1, p.213-285, 2 December 2003 [doi>10.1016/S0304-3975(03)00240-8]
• 45: Straßburger, L. and Lamarche, F. 2004. On proof nets for multiplicative linear logic with units. In Proceedings of the International Workshop on Computer Science Logic (CSL'04), J. Marcinkowski and A. Tarlecki, Eds. Lecture Notes in Computer Science, vol. 3210. Springer-Verlag, 145--159. http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf.
• 46: Tiu, A. 2006a. A local system for intuitionistic logic. In Proceedings of the International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR), M. Hermann and A. Voronkov, Eds. Lecture Notes in Artificial Intelligence, vol. 4246. Springer, 242--256. http://users.rsise.anu.edu.au/~tiu/localint.pdf.
• 47: Tiu, A. 2006b. A system of interaction and structure II: The need for deep inference. Logical Methods Comput. Sci. 2, 2, 4:1--24. http://arxiv.org/pdf/cs.LO/0512036.
• 48: A. S. Troelstra , H. Schwichtenberg, Basic proof theory, Cambridge University Press, New York, NY, 1996

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Theory

Keywords:
Analyticity, Frege systems, Statman tautologies, calculus of structures, deep inference