• DocumentCode
    1995680
  • Title

    Rigid E&oarr;-unifiability is DEXPTIME-complete

  • Author

    Goubault, Jean

  • Author_Institution
    Bull SA Res. Center, Les Clayes sous Bois, France
  • fYear
    1994
  • fDate
    4-7 Jul 1994
  • Firstpage
    498
  • Lastpage
    506
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
  • Conference_Location
    Paris
  • Print_ISBN
    0-8186-6310-3
  • Type

    conf

  • DOI
    10.1109/LICS.1994.316041
  • Filename
    316041
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1995680