Skip to main content
SpringerLink
Log in

E-unifiability via Narrowing

  • Conference paper
  • First Online:
Book cover Theoretical Computer Science (ICTCS 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2202))

Included in the following conference series:

Abstract

We formulate a narrowing-based decision procedure for E-unifiability. Termination is obtained requiring a narrowing bound: a bound on the length of narrowing sequences. We study general conditions under which the method guarantees that E-unifiability is in NP. The procedure is also extended to narrowing modulo AC (associativity and commutativity). As an application of our method, we prove NP-completeness of unifiability modulo bisimulation in process algebra with proper iteration, significantly extending a result in [8]. We also give (new) proofs, under a unified point of view, of NP-decidability of I, ACI, ACI1-unifiability and of unifiability in quasi-groups and central groupoids.

Work carried out within the MURST project TOSCA (Theory of concurrency, higher order and types)

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. F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories: combining decision procedures. Journal of Symbolic Computation, 21(2):211–244, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  2. F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.

    Google Scholar 

  3. F. Baader, W. Snyder. Unification theory. In A. Robinson and A. Voronkov, editors, Handbook of automated reasoning, Elsevier Science Publishers B. V., 1999.

    Google Scholar 

  4. J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge University Press, 1990.

    Google Scholar 

  5. H.-J. Bürckert. A resolution principle for a logic with restricted quantifiers. LNAI vol. 568, Springer Verlag, 1991.

    Google Scholar 

  6. A. Colmerauer. An introduction to PROLOG III. C. ACM 33, 69–90, 1990.

    Article  Google Scholar 

  7. W. Fokkink. A complete equational axiomatization for prefix iteration. Information processing letters, 52(6):333–337, 1994.

    Article  MathSciNet  Google Scholar 

  8. Q. Guo, P. Narendran, and S. K. Shukla. Unification and Matching in process Algebras. In T. Nipkow, editor, Proceedings of 9th RTA, LNCS vol. 1379, 1998.

    Google Scholar 

  9. J.-M. Hullot. Canonical forms and unification. In W. Bibel and R. Kowalski, editors, Proceedings of the 5th International Conference on Automated Deduction, LNCS vol. 87, 318–334, 1980.

    Google Scholar 

  10. B. Intrigila, M. Venturini Zilli and E. Viola. Unification problems over process languages. Technical Report SI-00/01. Dipartimento di Scienze dell’Informazione, University of Rome “La Sapienza”, Rome, 2000.

    Google Scholar 

  11. J.-P. Jouannaud, C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of A. Robinson, MIT Press, Cambridge, MA, 1991.

    Google Scholar 

  12. D. Kapur and P. Narendran. Complexity of unification problems with associativecommutative operators. J. Automated Reasoning 9:261–288, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. D. Kapur and P. Narendran. Matching, unification and complexity. SIGSAM Bulletin, 1987.

    Google Scholar 

  14. D. Kapur and P. Narendran. Double exponential complexity of computing complete sets of AC-unifiers. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, 11–21, 1992.

    Google Scholar 

  15. C. Kirchner, H. Kirchner and M. Rusinowitch. Deduction with symbolic constraints. Revue d’Intelligence Artificielle (Special issue on Automatic Deduction), 4(3):9–52, 1990.

    Google Scholar 

  16. P. Narendran. Unification modulo ACI+1+0. Fundamenta Informaticae, 25(1):49–57, 1996.

    MATH  MathSciNet  Google Scholar 

  17. R. Nieuwenhuis. On Narrowing, Refutation proofs and Constraints. In J. Hsiang, editor, Proceedings of 6th RTA, LNCS vol. 914, 1995.

    Google Scholar 

  18. R. Nieuwenhuis. Decidability and Complexity Analysis by Basic Paramodulation. Information and Computation 147:1–21, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  19. M. Paterson, M. Wegman. Linear unification. Journal of Computer and System Sciences, 16(2):158–167, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  20. G. Peterson, M. Stickel. Complete sets of reductions for equational theories with complete unification algorithms. Journal of the ACM 28(2):233–264, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  21. G. Plotkin. Building-in Equational Theories. Machine Intelligence, 7:73–90 1972.

    MATH  MathSciNet  Google Scholar 

  22. L. Vigneron. Automated Deduction Techniques for Studying Rough Algebras. Fundamenta Informaticae 33, 85–103, 1998.

    MATH  MathSciNet  Google Scholar 

  23. E. Viola. E-unificabilità: decidibilità, complessità e algebre di processi. B. S. Thesis, Dipartimento di Scienze dell’Informazione, University of Rome “La Sapienza”, Rome, 2000.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Scienze dell’Informazione, Univ. di Roma “La Sapienza”, V. Salaria 113, 00198, Roma, Italy

    Emanuele Viola

Authors
  1. Emanuele Viola
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Viola, E. (2001). E-unifiability via Narrowing. In: Theoretical Computer Science. ICTCS 2001. Lecture Notes in Computer Science, vol 2202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45446-2_27

Download citation

  • DOI: https://doi.org/10.1007/3-540-45446-2_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42672-1

  • Online ISBN: 978-3-540-45446-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation