Asymmetric unification and disunification

DOI10.1007/978-3-030-22102-7_23MaRDI QIDQ2185487zbMATH OpenOpenAlexFDO

Authors Kimberly A. Cornell, Paliath Narendran, V. Ravishankar

Publication date 4 June 2020

Full work available at URL https://arxiv.org/abs/1706.05066

zbMATH Keywords

disunificationasymmetric unificationtime-complexity analysis

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

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.

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

(3)

• Nominal equational problems
• On asymmetric unification for the theory of XOR with a homomorphism
• On solving nominal disunification constraints

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)