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

Authors: Jean Goubault-Larrecq

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{GoubaultLarrecq-RigidEunifiabilityi,
    author = 	 {Jean Goubault-Larrecq},
    title = 	 {Rigid E-unifiability is DEXPTIME-complete},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {498--506},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }