Title :
Rigid E&oarr;-unifiability is DEXPTIME-complete
Author_Institution :
Bull SA Res. Center, Les Clayes sous Bois, France
Abstract :
Proves that rigid E&oarr;-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
Keywords :
computational complexity; decidability; DEXPTIME-completeness; PSPACE-completeness; decision problem; equality; first-order logic; first-order tableaux-like proof procedures; monadic terms; rigid E&oarr;-unifiability; Boolean functions; Calculus; Data structures; Equations; Logic;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316041
