We give an algorithm for deciding E-unification problems for linear standard equational theories (linear equations with all shared variables at a depth less than two) and varity 1 goals (linear equations with no shared variables). We show that the algorithm halts in quadratic time for the non-uniform E-unification problem, and linear time if the equational theory is varity 1. The algorithm is still polynomial for the uniform problem. The size of the complete set of unifiers is exponential, but membership in that set can be determined in polynomial time. For any goal (not just varity 1) we give a NEXPTIME algorithm. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Lynch, C., & Morawska, B. (2001). Complexity of linear standard theories. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2250, 186–200. https://doi.org/10.1007/3-540-45653-8_13
Mendeley helps you to discover research relevant for your work.