Logic in Computer Science (LICS 1994)

Paper: Rigid E-unifiability is DEXPTIME-complete (at LICS 1994)

Authors: Jean Goubault

Abstract

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}
  }