On the Sequential Nature of Unification
The problem of unification of terms is log-space complete for P. In deriving this lower bound no use is made of the potentially concise representation of terms by directed acyclic graphs. In addition, the problem remains complete even if infinite substitutions are allowed. A consequence of this resu...
Main Authors: | , , |
---|---|
Published: |
2023
|
Online Access: | https://hdl.handle.net/1721.1/149067 |