Skip to main content
SpringerLink
Log in

Modular Termination of Basic Narrowing

  • Conference paper
Rewriting Techniques and Applications (RTA 2008)

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

Included in the following conference series:

Abstract

Basic narrowing is a restricted form of narrowing which constrains narrowing steps to a set of non-blocked (or basic) positions. Basic narrowing has a number of important applications including equational unification in canonical theories. Another application is analyzing termination of narrowing by checking the termination of basic narrowing, as done in pioneering work by Hullot. In this work, we study the modularity of termination of basic narrowing in hierarchical combinations of TRSs, including a generalization of proper extensions with shared subsystem. This provides new algorithmic criteria to prove termination of basic narrowing.

This work has been partially supported by the EU (FEDER) and Spanish MEC project TIN2007-68093-C02-02, Integrated Action Hispano-Alemana A2006-0007, the UPV grant 3249 PAID0607 and the UPV grant FPI-UPV 2006-01.

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. Alpuente, M., Escobar, S., Iborra, J.: Modular termination of basic narrowing. Technical Report DSIC-II/04/08, Universidad Politécnica de Valencia (2007)

    Google Scholar 

  2. Alpuente, M., Escobar, S., Iborra, J.: Termination of Narrowing revisited. Theoretical Computer Science (to appear, 2008)

    Google Scholar 

  3. Alpuente, M., Falaschi, M., Gabbrielli, M., Levi, G.: The semantics of equational logic programming as an instance of CLP. In: Logic Programming Languages, pp. 49–81. The MIT Press, Cambridge (1993)

    Google Scholar 

  4. Alpuente, M., Falaschi, M., Levi, G.: Incremental Constraint Satisfaction for Equational Logic Programming. Theoretical Computer Science 142(1), 27–57 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  5. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1-2), 133–178 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Proc. of the 8th Int’l Conf. on Automated Deduction, January 1986, pp. 5–20 (1986)

    Google Scholar 

  7. Comon-Lundh, H.: Intruder Theories (Ongoing Work). In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 1–4. Springer, Heidelberg (2004)

    Google Scholar 

  8. Cortier, V., Delaune, S., Lafourcade, P.: A Survey of Algebraic Properties used in Cryptographic Protocols. Journal of Computer Security 14(1), 1–43 (2006)

    Google Scholar 

  9. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol. B, pp. 244–320. Elsevier Science, Amsterdam (1990)

    Google Scholar 

  10. Escobar, S., Meadows, C., Meseguer, J.: A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties. TCS 367 (2006)

    Google Scholar 

  11. Escobar, S., Meseguer, J.: Symbolic model checking of infinite-state systems using narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Fay, M.: First-Order Unification in an Equational Theory. In: Fourth Int’l Conf. on Automated Deduction, pp. 161–167 (1979)

    Google Scholar 

  13. Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming 19&20, 583–628 (1994)

    Article  MathSciNet  Google Scholar 

  14. Hölldobler, S. (ed.): Foundations of Equational Logic Programming. LNCS, vol. 353. Springer, Heidelberg (1989)

    MATH  Google Scholar 

  15. Hullot, J.-M.: Canonical Forms and Unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)

    Google Scholar 

  16. Hullot, J.-M.: Compilation de Formes Canoniques dans les Théories q́uationelles. Thése de Doctorat de Troisième Cycle. PhD thesis, Université de Paris Sud, Orsay (France) (1981)

    Google Scholar 

  17. Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 158–200. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  18. Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. HOSC, 123–160 (2007)

    Google Scholar 

  19. Middeldorp, A., Hamoen, E.: Completeness Results for Basic Narrowing. J. of Applicable Algebra in Engineering, Comm. and Computing 5, 313–353 (1994)

    MathSciNet  Google Scholar 

  20. Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  21. Prehofer, C.: On Modularity in Term Rewriting and Narrowing. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol. 845, pp. 253–268. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  22. Krishna Rao, M.R.K.: Modular proofs for completeness of hierarchical term rewriting systems. Theoretical Computer Science (January 1995)

    Google Scholar 

  23. Réty, P.: Improving Basic Narrowing Techniques. In: Lescanne, P. (ed.) RTA 1987. LNCS, vol. 256. Springer, Heidelberg (1987)

    Google Scholar 

  24. TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  25. Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett. 25(3), 141–143 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  26. Urbain, X.: Modular & incremental automated termination proofs. Int. J. Approx. Reasoning 32(4), 315–355 (2004)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Politécnica de Valencia, Spain

    María Alpuente, Santiago Escobar & José Iborra

Authors
  1. María Alpuente
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Santiago Escobar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. José Iborra
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alpuente, M., Escobar, S., Iborra, J. (2008). Modular Termination of Basic Narrowing. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70590-1_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70588-8

  • Online ISBN: 978-3-540-70590-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation