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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci |
| Place of Publication | Piscataway, NJ, United States |
| Publisher | IEEE |
| Pages | 503-512 |
| Number of pages | 9 |
| Publication status | Published - 1996 |
| Event | Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96 - New Brunswick, NJ, USA Duration: 1 Jul 1996 → … http://dblp.uni-trier.de/db/conf/lics/lics96.html#DegtyarevV96http://dblp.uni-trier.de/rec/bibtex/conf/lics/DegtyarevV96.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/lics/DegtyarevV96 |
Conference
| Conference | Proceedings of the 1996 11th Annual IEEE Symposium on Logic in Computer Science, LICS'96 |
|---|---|
| City | New Brunswick, NJ, USA |
| Period | 1/07/96 → … |
| Internet address |