Asymmetric unification and disunification
From MaRDI portal
Publication:2185487
DOI10.1007/978-3-030-22102-7_23zbMATH Open1444.68088arXiv1706.05066OpenAlexW2962992940MaRDI QIDQ2185487FDOQ2185487
Authors: Kimberly A. Cornell, Paliath Narendran, V. Ravishankar 
Publication date: 4 June 2020
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 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.
Full work available at URL: https://arxiv.org/abs/1706.05066
Recommendations
- On Asymmetric Unification and the Combination Problem in Disjoint Theories
- Asymmetric unification: a new unification paradigm for cryptographic protocol analysis
- On solving equations and disequations
- On asymmetric unification for the theory of XOR with a homomorphism
- Narrowing based procedures for equational disunification
Cited In (2)
This page was built for publication: Asymmetric unification and disunification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2185487)
