Second-order proof systems for algebraic specification languages

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as term-generation or initiality. For proving properties of specifications and refining them to programs, an axiomatisation of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for most algebraic specification languages. In this paper, we construct non-effective second-order axiomatizations for constraints commonly found in specification languages, and simplified forms useful for the universal fragment. They are shown to be sound and complete, but not effective, since the underlying second-order logic is not effective. A good level of machine support is still possible using higherorder proof assistants.

langue originaleAnglais
titreRecent Trends in Data Type Specification - 9th Workshop on Specification of Abstract Data Types Joint with the 4th COMPASS Workshop, Selected Papers
EditeurSpringer Verlag
Pages321-336
Nombre de pages16
ISBN (imprimé)9783540578673
Etat de la publicationPublié - 1 janv. 1994
Evénement9th Workshop on Specification of Abstract Data Types joint with 4th COMPASS Workshop, 1992 - Caldes de Malavella, Espagne
Durée: 26 oct. 199230 oct. 1992

Série de publications

NomLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume785 LNCS
ISSN (imprimé)0302-9743
ISSN (Electronique)1611-3349

Une conférence

Une conférence9th Workshop on Specification of Abstract Data Types joint with 4th COMPASS Workshop, 1992
Pays/TerritoireEspagne
La villeCaldes de Malavella
période26/10/9230/10/92

Empreinte digitale

Examiner les sujets de recherche de « Second-order proof systems for algebraic specification languages ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation