Paper: Rigid E-unifiability is DEXPTIME-complete (at LICS 1994)
Authors: Jean GoubaultAbstract
Proves that rigid E-unifiability, a decision problem invented by Gallier et al. (1987) to extend first-order tableaux-like proof procedures to first-order logic with equality, is DEXPTIME-complete; and that, when restricted to monadic terms, it is PSPACE-complete
BibTeX
@InProceedings{Goubault-RigidEunifiabilityi, author = {Jean Goubault}, title = {Rigid E-unifiability is DEXPTIME-complete}, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {498--506}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }