Abstract
We compare two kinds of unification problems: Asymmetric Unification and Disunification, which are variants of Equational Unification. Asymmetric Unification is a type of Equational Unification where the instances of the right-hand sides of the equations are in normal form with respect to the given term rewriting system. In Disunification we solve equations and disequations with respect to an equational theory for the case with free constants. We contrast the time complexities of both and show that the two problems are incomparable: there are theories where one can be solved in polynomial time while the other is NP-hard. This goes both ways. The time complexity also varies based on the termination ordering used in the term rewriting system.
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
Similar content being viewed by others
Notes
References
Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121–123 (1979)
Baader, F.: Unification in commutative theories. J. Symb. Comput. 8(5), 479–497 (1989)
Baader, F.: Unification in commutative theories, Hilbert’s basis theorem, and Gröbner bases. J. ACM 40(3), 477–503 (1993)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)
Baader, F., Nutt, W.: Combination problems for commutative/monoidal theories or how algebra can help in equational unification. Appl. Algebra Eng. Commun. Comput. 7(4), 309–337 (1996)
Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229–255 (1995)
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol. 1, pp. 445–532 (2001)
Bachmair, L.: Canonical Equational Proofs. Birkhauser, Boston (1991)
Bogdanov, A., Mertens, M.C., Paar, C., Pelzl, J., Rupp, A.: A parallel hardware architecture for fast Gaussian elimination over GF(2). In: 14th IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM 2006), Napa, CA, USA, 24–26 April 2006, Proceedings, pp. 237–248. IEEE Computer Society (2006)
Brahmakshatriya, S., Danturi, S., Gero, K.A., Narendran, P.: Unification problems modulo a theory of until. In: Korovin, K., Morawska, B. (eds.) 27th International Workshop on Unification, UNIF 2013, Eindhoven, Netherlands, 26 June 2013. EPiC Series in Computing, vol. 19, pp. 22–29. EasyChair (2013). http://www.easychair.org/publications/?page=723757558
Büchi, J.R.: Weak second-order arithmetic and finite automata. Math. Logic Q. 6(1–6), 66–92 (1960)
Buntine, W.L., Bürckert, H.-J.: On solving equations and disequations. J. ACM 41(4), 591–629 (1994)
Bürckert, H.-J., Herold, A., Schmidt-Schauss, M.: On equational theories, unification, and (un)decidability. J. Symb. Comput. 8(1–2), 3–49 (1989)
Comon, H.: Disunification: a survey. In: Lassez, J.-L., Plotkin, G.D. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 322–359. The MIT Press (1991)
Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98(1), 21–51 (1961)
Erbatur, S., et al.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231–248. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_16
Erbatur, S., Kapur, D., Marshall, A.M., Meadows, C., Narendran, P., Ringeissen, C.: On asymmetric unification and the combination problem in disjoint theories. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 274–288. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54830-7_18
Garey, M., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1979)
Greenwell, R.N., Kertzner, S.: Solving linear diophantine matrix equations using the Smith normal form (more or less). Int. J. Pure Appl. Math. 55(1), 49–60 (2009)
Guo, Q., Narendran, P., Wolfram, D.A.: Complexity of nilpotent unification and matching problems. Inf. Comput. 162(1–2), 3–23 (2000)
Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 257–321 (1991)
Kaltofen, E., Krishnamoorthy, M.S., Saunders, B.D.: Fast parallel computation of Hermite and Smith forms of polynomial matrices. SIAM J. Algebraic Discrete Methods 8(4), 683–690 (1987)
Kannan, R.: Solving systems of linear equations over polynomials. Theor. Comput. Sci. 39, 69–88 (1985)
Klaedtke, F., Ruess, H.: Parikh automata and monadic second-order logics with linear cardinality constraints (2002)
Koç, Ç.K., Arachchige, S.N.: A fast algorithm for Gaussian elimination over GF(2) and its implementation on the GAPP. J. Parallel Distrib. Comput. 13(1), 118–122 (1991)
Liu, Z.: Dealing efficiently with exclusive-OR, abelian groups and homomorphism in cryptographic protocol analysis. Ph.D. thesis, Clarkson University (2012)
Lynch, C., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45620-1_37
MacDuffee, C.C.: The Theory of Matrices. Chelsea Publishing Company, New York (1961)
Nutt, W.: Unification in monoidal theories. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 618–632. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52885-7_118
Rotman, J.J.: Advanced Modern Algebra. Prentice Hall. 1st edn (2002); 2nd printing (2003)
Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. Logic Automata 2, 629–736 (2008)
Acknowledgements
We wish to thank Franz Baader for all his remarkable contributions in this field. We also wish to thank the anonymous reviewers for their detailed comments and suggestions which helped us greatly in improving this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ravishankar, V., Cornell, K.A., Narendran, P. (2019). Asymmetric Unification and Disunification. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, AY., Wolter, F. (eds) Description Logic, Theory Combination, and All That. Lecture Notes in Computer Science(), vol 11560. Springer, Cham. https://doi.org/10.1007/978-3-030-22102-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-22102-7_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-22101-0
Online ISBN: 978-3-030-22102-7
eBook Packages: Computer ScienceComputer Science (R0)