Paper: Decidability Problems for the Prenex Fragment of Intuitionistic Logic (at LICS 1996)

Authors: Anatoli Degtyarev Andrei Voronkov

Abstract

We develop a constraint-based technique which allows one to prove decidability and complexity results for sequent calculi. Specifically, we study decidability problems for the prenex fragment of intuitionistic logic. We introduce an analogue of Skolemization for intuitionistic logic with equality, prove PSPACE-completeness of two fragments of intuitionistic logic with and without equality and some other results. In the proofs, we use a combination of techniques of constraint satisfaction, loop-free sequent systems of intuitionistic logic and properties of simultaneous rigid E-unification

BibTeX

  @InProceedings{DegtyarevVoronkov-DecidabilityProblem,
    author = 	 {Anatoli Degtyarev and Andrei Voronkov},
    title = 	 {Decidability Problems for the Prenex Fragment of Intuitionistic Logic},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {503--512},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }