Abstract
The calculus of structures is a proof theoretical formalism which generalizes the sequent calculus with the feature of deep inference: In contrast to the sequent calculus, inference rules can be applied at any depth inside a formula, bringing shorter proofs than any other formalisms supporting analytical proofs. However, deep applicability of the inference rules causes greater nondeterminism than in the sequent calculus regarding proof search. In this paper, we introduce a new technique which reduces nondeterminism without breaking proof theoretical properties and provides a more immediate access to shorter proofs. We present this technique on system BV, the smallest technically non-trivial system in the calculus of structures, extending multiplicative linear logic with the rules mix, nullary mix, and a self-dual non-commutative logical operator. Because our technique exploits a scheme common to all the systems in the calculus of structures, we argue that it generalizes to these systems for classical logic, linear logic, and modal logics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andreoli, J.-M.: Logic programming with focussing proofs in linear logic. Journal of Logic and Compututation 2(3), 297–347 (1992)
Brünnler, K.: Deep Inference and Symmetry in Classical Proofs. PhD thesis, TU Dresden (2003)
Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001)
Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 302–316. Springer, Heidelberg (2002)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, p. 240. Springer, Heidelberg (1999)
Guglielmi, A.: A system of interaction and structure. Technical Report WV-02-10, TU Dresden (2002); ACM Transactions on Computational Logic (accepted, 2002)
Guglielmi, A.: Polynomial size deep-inference proofs instead of exponential size shallow-inference proofs (2004), Available on the web at: http://cs.bath.ac.uk/ag/p/AG12.pdf
Guglielmi, A., Straßburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 54–68. Springer, Heidelberg (2001)
Guglielmi, A., Straßburger, L.: A non-commutative extension of MELL. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS, vol. 2514, pp. 231–246. Springer, Heidelberg (2002)
Kahramanoğulları, O.: Implementing system BV of the calculus of structures in Maude. In: Alonso i Alemany, L., Égré, P. (eds.) Proc. of the ESSLLI-2004 Student Session, Université Henri Poincaré, Nancy, France, pp. 117–127 (2004)
Kahramanoğulları, O.: System BV without the equalities for unit. In: Aykanat, C., Dayar, T., Körpeoğlu, İ. (eds.) ISCIS 2004. LNCS, vol. 3280, pp. 986–995. Springer, Heidelberg (2004)
Kahramanoğulları, O.: Reducing nondeterminism in the calculus of structures.Technical Report WV-06-01, TU Dresden (2006), Available at: http://www.ki.inf.tu-dresden.de/~ozan/redNondet.pdf
Kahramanoğulları, O.: System BV is NP-complete. In: de Queiroz, R., Macintyre, A., Bittencourt, G. (eds.) WoLLIC 2005, Florianapolis, Brazil. ENTCS, vol. 143, pp. 87–99. Elsevier, Amsterdam (2006)
Kahramanoğulları, O., Moreau, P.-E., Reilles., A.: Implementing deep inference in TOM. In: Bruscoli, P., Lamarche, F., Stewart, C. (eds.) Structures and Deduction 2005 (ICALP 2005 Workshop), pp. 158–172 (2005)
Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165, 201–232 (1996)
Moreau, P.-E., Ringeissen, C., Vittek, M.: A pattern matching compiler for multiple target languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 61–76. Springer, Heidelberg (2003)
Retoré, C.: Pomset logic: A non-commutative extension of classical linear logic. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 300–318. Springer, Heidelberg (1997)
Stewart, C., Stouppa, P.: A systematic proof theory for several modal logics. In: Schmidt, R., Pratt-Hartmann, I., Reynolds, M., Wansing, H. (eds.) Advances in Modal Logic, vol. 5, pp. 309–333. King’s College Publications (2005)
Straßburger, L.: A local system for linear logic. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS, vol. 2514, pp. 388–402. Springer, Heidelberg (2002)
Straßburger, L.: Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, TU Dresden (2003)
Straßburger, L.: System NEL is undecidable. In: de Queiroz, R., Pimentel, E., Figueiredo, L. (eds.) WoLLIC 2003. ENTCS, vol. 84. Elsevier, Amsterdam (2003)
Tiu, A.F.: A local system for intuitionistic logic. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 242–256. Springer, Heidelberg (2006)
Tiu, A.F.: A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science (to appear, 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kahramanoğulları, O. (2006). Reducing Nondeterminism in the Calculus of Structures. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_19
Download citation
DOI: https://doi.org/10.1007/11916277_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)