Abstract
We define a subclass of the class of linear equational theories, called finitely closable linear theories. We consider unification problems with no repeated variables. We show the decidability of this subclass, and give an algorithm in PSPACE. If all function symbols are monadic, then the running time is in NP, and quadratic for unitary monadic finitely closable linear theories. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Lynch, C., & Morawska, B. (2001). Decidability and complexity of finitely closable linear equational theories. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2083, 499–513. https://doi.org/10.1007/3-540-45744-5_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
