Skip to main content
SpringerLink
Log in

Axiom Directed Focusing

  • Conference paper
Types for Proofs and Programs (TYPES 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5497))

Included in the following conference series:

Abstract

Superdeduction and deduction modulo are two methods designed to ease the use of first-order theories in predicate logic. Superdeduction modulo combines both in a single framework. Although soundness is ensured, using superdeduction modulo to extend deduction with awkward theories can jeopardize cut-elimination or completeness w.r.t predicate logic. In this paper our aim is to design criteria for theories which will ensure these properties. We revisit the superdeduction paradigm by comparing it with the focusing approach. In particular we prove a focalization theorem for cut-free superdeduction modulo: we show that permutations of inference rules can transform any cut-free proof in deduction modulo into a cut-free proof in superdeduction modulo and conversely, provided that some hypotheses on the synchrony of reasoning axioms are verified. It implies that cut-elimination for deduction modulo and for superdeduction modulo are equivalent. Since several criteria have already been proposed for theories that do not break cut-elimination of the corresponding deduction modulo system, these criteria also imply cut-elimination of the superdeduction modulo system, provided our synchrony hypotheses hold.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  2. Brauner, P., Houtmann, C., Kirchner, C.: Principles of superdeduction. In: Ong, L. (ed.) Proceedings of LICS, July 2007, pp. 41–50 (2007)

    Google Scholar 

  3. Girard, J.Y.: On the meaning of logical rules II : multiplicatives and additives. In: Bauer, Steinbrüggen (eds.) Foundation of Secure Computation, pp. 183–212. IOS Press, Amsterdam (2000)

    Google Scholar 

  4. Andreoli, J.M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dowek, G., Werner, B.: Proof normalization modulo. Journal of Symbolic Logic 68(4), 1289–1316 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  6. Dowek, G.: Truth values algebras and proof normalization. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 110–124. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Dowek, G., Hermant, O.: A simple proof that super-consistency implies cut elimination. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 93–106. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Hermant, O.: Méthodes Sémantiques en Déduction Modulo. PhD thesis, École Polytechnique (2005)

    Google Scholar 

  9. Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 221–233. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Burel, G., Kirchner, C.: Cut elimination in deduction modulo by abstract completion. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 115–131. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Huang, X.: Reconstruction proofs at the assertion level. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 738–752. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  12. Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bulletin of Symbolic Logic 4(4), 418–435 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  13. Hallnäs, L., Schroeder-Heister, P.: A proof-theoretic approach to logic programming. II. programs as definitions. Journal of Logic and Computation 1(5), 635–660 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  14. McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science 232(1-2), 91–119 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Brauner, P., Houtmann, C., Kirchner, C.: Superdeduction at work. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol. 4600, pp. 132–166. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ: an intentional first-order expression of higher-order logic. Math. Struct. in Comp. Science 11(1), 21–45 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  17. Dowek, G.: Proof normalization for a first-order formulation of higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 105–119. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Ronchi Della Rocca, S. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  19. Burel, G.: Superdeduction as a logical framework. In: LICS 2008 (accepted, 2008)

    Google Scholar 

  20. Burel, G.: Unbounded proof-length speed-up in deduction modulo. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 496–511. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  21. Bonichon, R.: TaMeD: A tableau method for deduction modulo. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS, vol. 3097, pp. 445–459. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  22. Houtmann, C.: Axiom directed focusing. Long version (2008), http://hal.inria.fr/inria-00212059/en/

  23. Dowek, G.: La part du calcul. Mémoire d’habilitation, Université de Paris 7 (1999)

    Google Scholar 

  24. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logic. In: TCS (March 2008) (accepted)

    Google Scholar 

  25. Miller, D., Saurin, A.: From proofs to focused proofs: A modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 405–419. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Andreoli, J.M.: Focussing and proof construction. Annals Pure Applied Logic 107(1-3), 131–163 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  27. Kleene, S.C.: Permutability of inferences in Gentzen’s calculi LK and LJ. In: Two Papers on the Predicate Calculus, pp. 1–26. American Mathematical Society (1952)

    Google Scholar 

  28. Hermant, O.: A model-based cut elimination proof. In: 2nd St-Petersburg Days of Logic and Computability (2003)

    Google Scholar 

  29. Brauner, P., Dowek, G., Wack, B.: Normalization in supernatural deduction and in deduction modulo (2007) (available on the author’s webpage)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Henri Poincaré Nancy 1 & LORIA, Campus Scientifique, BP 239, 54506, Vandoeuvre-lès-Nancy Cedex, France

    Clément Houtmann

Authors
  1. Clément Houtmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Stefano Berardi  & Ugo de’Liguoro  & 

  2. Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Ferruccio Damiani

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Houtmann, C. (2009). Axiom Directed Focusing. In: Berardi, S., Damiani, F., de’Liguoro, U. (eds) Types for Proofs and Programs. TYPES 2008. Lecture Notes in Computer Science, vol 5497. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02444-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02444-3_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02443-6

  • Online ISBN: 978-3-642-02444-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation