Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Negativ set constraints: an easy proof of decidability

Charatonik, W., & Pacholski, L.(1993). Negativ set constraints: an easy proof of decidability (MPI-I-93-265). Saarbrücken: Max-Planck-Institut für Informatik.

Item is

Dateien

einblenden: Dateien
ausblenden: Dateien
:
MPI-I-93-265.pdf (beliebiger Volltext), 109KB
Name:
MPI-I-93-265.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Öffentlich
MIME-Typ / Prüfsumme:
application/pdf / [MD5]
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Charatonik, Witold1, Autor           
Pacholski, Leszek1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Systems of set constraints describe relations between sets of ground terms. They have been successfuly used in program analysis and type inference. So far two proofs of decidability of mixed set constraints have been given: by R.~Gilleron, S.~Tison and M.~Tommasi [12] and A.~Aiken, D.~Kozen, and E.L.~Wimmers [3], but both these proofs are very long, involved and difficult to follow. We first give a new, simple proof of decidability of systems of mixed positive and negative set constraints. We explicitely describe a very simple algorithm working in NEXPTIME and we give in all detail a relatively easy proof of its correctness. Then we sketch how our technique can be applied to get various extensions of this result. In particular we prove that the problem of consistency of mixed set constraints with restricted projections and unrestricted diagonalization is decidable. Diagonalization here represents a decidable part of equality. It is known that the equality of terms can not be directly included in the language of set constraints. Our approach is based on a reduction of set constraints to the monadic class given in a recent paper by L.~Bachmair, H.~Ganzinger, and U.~Waldmann [7]. To save space we assume that the reader is familiar with the main ideas of the method introduced in [7] of using the monadic class to study set constraints. We shall drop this assumption in the full paper.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 1993
 Publikationsstatus: Erschienen
 Seiten: 11 p.
 Ort, Verlag, Ausgabe: Saarbrücken : Max-Planck-Institut für Informatik
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: URI: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/93-265
Reportnr.: MPI-I-93-265
BibTex Citekey: CharatonikPacholski93
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Research Report / Max-Planck-Institut für Informatik
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: - Identifikator: -