Logic in Computer Science (LICS 1996)

Paper: Simultaneous Rigid E-Unification and Related Algorithmic Problems (at LICS 1996)

Authors: Anatoli Degtyarev Yuri Matiyasevich Andrei Voronkov

Abstract

The notion of simultaneous rigid E-unification was introduced in 1987 in the area of automated theorem proving with equality in sequent-based methods, for example the connection method or the tableau method. Recently, simultaneous rigid E-unification was shown undecidable. Despite the importance of this notion, for example in theorem proving in intuitionistic logic, very little is known of its decidable fragments. We prove decidability results for fragments of monadic simultaneous rigid E-unification and show the connections between this notion and some algorithmic problems of logic and computer science.

BibTeX

  @InProceedings{DegtyarevMatiyasevi-SimultaneousRigidEU,
    author = 	 {Anatoli Degtyarev and Yuri Matiyasevich and Andrei Voronkov},
    title = 	 {Simultaneous Rigid E-Unification and Related Algorithmic Problems},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {494-502},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }