Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2019: Automated Deduction – CADE 27 pp 1–17Cite as

Unification Modulo Lists with Reverse Relation with Certain Word Equations

  • Conference paper
  • First Online:

  • 644 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11716))

Abstract

Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

This is a preview of subscription content, 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   69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   89.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

Learn about institutional subscriptions

References

  1. Anantharaman, S., Hibbs, P., Narendran, P., Rusinowitch, M.: Unification of lists with reverse as solving simple sets of word equations. Research-Report. https://hal.archives-ouvertes.fr/hal-02123648

  2. Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150–166. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_10

    Chapter  Google Scholar 

  3. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1–4:51 (2009)

    Article  MathSciNet  Google Scholar 

  4. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  5. Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symb. Comput. 21(2), 211–243 (1996)

    Article  MathSciNet  Google Scholar 

  6. Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 445–532. Elsevier and MIT Press (2001)

    Google Scholar 

  7. Colmerauer, A.: An introduction to Prolog III. Commun. ACM 33(7), 69–90 (1990)

    Article  Google Scholar 

  8. Dabrowski, R., Plandowski, W.: On word equations in one variable. Algorithmica 60(4), 819–828 (2011)

    Article  MathSciNet  Google Scholar 

  9. Diekert, V., Jez, A., Plandowski, W.: Finding all solutions of equations in free groups and monoids with involution. Inf. Comput. 251, 263–286 (2016)

    Article  MathSciNet  Google Scholar 

  10. Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. Commun. ACM 21(12), 1048–1064 (1978)

    Article  MathSciNet  Google Scholar 

  11. Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209–226. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_21

    Chapter  Google Scholar 

  12. Hibbs, P.: Unification modulo common list functions. Doctoral Dissertation. University at Albany–SUNY (2015)

    Google Scholar 

  13. Kapur, D.: Towards a theory for abstract data types. Doctoral Dissertation. Massachusetts Institute of Technology (1980)

    Google Scholar 

  14. Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. 31(2), 125–157 (1987)

    Article  MathSciNet  Google Scholar 

  15. Karhumäki, J.: Combinatorics on Words: A New Challenging Topic, p. 12. Turku Centre for Computer Science, Turku (2004)

    MATH  Google Scholar 

  16. Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS, vol. 9322, pp. 135–150. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24246-0_9

    Chapter  Google Scholar 

  17. Lin, A.W., Majumdar, R.: Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility. arXiv preprint arXiv:1805.06701 (2018)

  18. Morita, K.: Universality of a reversible two-counter machine. Theoret. Comput. Sci. 168(2), 303–320 (1996)

    Article  MathSciNet  Google Scholar 

  19. Musser, D.R.: Abstract data type specification in the AFFIRM system. IEEE Trans. Softw. Eng. 6(1), 24–32 (1980)

    Article  MathSciNet  Google Scholar 

  20. Musser, D.R.: On proving inductive properties of abstract data types. In: Proceedings of the Seventh Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 154–162 (1980)

    Google Scholar 

  21. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)

    Article  Google Scholar 

  22. Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM 27(3), 403–411 (1980)

    Article  MathSciNet  Google Scholar 

  23. Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the ACM Symposium on the Theory of Computing, pp. 467–476 (2006)

    Google Scholar 

  24. Robson, J.M., Diekert, V.: On quadratic word equations. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 217–226. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49116-3_20

    Chapter  Google Scholar 

  25. Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984)

    Article  MathSciNet  Google Scholar 

  26. Schulz, K.U.: On existential theories of list concatenation. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 294–308. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0022264

    Chapter  Google Scholar 

Download references

Author information

Author notes

  1. Peter Hibbs

    Present address: Google Inc., Mountain View, USA

Authors and Affiliations

  1. LIFO - Université d’Orléans, Orléans, France

    Siva Anantharaman

  2. University at Albany–SUNY, Albany, USA

    Peter Hibbs & Paliath Narendran

  3. Loria-Inria Université de Lorraine, Nancy, France

    Michael Rusinowitch

Authors
  1. Siva Anantharaman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter Hibbs
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paliath Narendran
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Michael Rusinowitch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Siva Anantharaman .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Pascal Fontaine

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Anantharaman, S., Hibbs, P., Narendran, P., Rusinowitch, M. (2019). Unification Modulo Lists with Reverse Relation with Certain Word Equations. In: Fontaine, P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science(), vol 11716. Springer, Cham. https://doi.org/10.1007/978-3-030-29436-6_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29436-6_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29435-9

  • Online ISBN: 978-3-030-29436-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation