Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eleventh Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {494--502},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski