Abstract
Equational unification is an important research area with many applications, such as cryptographic protocol analysis. Unification modulo a convergent term rewrite system is undecidable, even with just a single rule. To identify decidable (and tractable) cases, two paradigms have been developed — Basic Syntactic Mutation [14] and the Finite Variant Property [6]. Inspired by the Basic Syntactic Mutation approach, we investigate the notion of forward closure along with suitable redundancy constraints. We show that a convergent term rewriting system R has a finite forward closure if and only if R has the finite variant property. We also show the undecidability of the finiteness of forward closure, therefore determining if a system has the finite variant property is undecidable.
C. Bouchard, K. Gero, and P. Narendran were supported in part by NSF grant CNS 09-05286. C. Lynch was supported in part by NSF grant CNS 09-05378.
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
Anantharaman, S., Erbatur, S., Lynch, C., Narendran, P., Rusinowitch, M.: Unification Modulo Synchronous Distributivity. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 14–29. Springer, Heidelberg (2012)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)
Baader, F., Snyder, W.: Unification Theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 440–526. Elsevier Science Publishers BV (1999)
Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On Forward Closure and the Finite Variant Property. Technical report, Dept. of Computer Science, University at Albany—SUNY (July 2013)
Bouchard, C., Gero, K.A., Narendran, P.: Some Notes on Basic Syntactic Mutation. In: Escobar, S., Korovin, K., Rybakov, V. (eds.) Proceedings 26th International Workshop on Unification, pp. 9–14 (2012)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73–90. Springer, Heidelberg (2012)
Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 79–93. Springer, Heidelberg (2008)
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming 81(7-8), 898–928 (2012); Rewriting Logic and its Applications
Hermann, M.: Chain properties of rule closures. Formal Aspects of Computing 2(1), 207–225 (1990)
Hillebrand, G.G., Kanellakis, P.C., Mairson, H.G., Vardi, M.Y.: Undecidable Boundedness Problems for Datalog Programs. Journal of Logic Programming 25(2), 163–190 (1995)
Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)
Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)
Lynch, C., Morawska, B.: Basic Syntactic Mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002)
Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier, MIT Press (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouchard, C., Gero, K.A., Lynch, C., Narendran, P. (2013). On Forward Closure and the Finite Variant Property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-40885-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40884-7
Online ISBN: 978-3-642-40885-4
eBook Packages: Computer ScienceComputer Science (R0)