Second-order proof systems for algebraic specification languages

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationRecent Trends in Data Type Specification - 9th Workshop on Specification of Abstract Data Types Joint with the 4th COMPASS Workshop, Selected Papers
PublisherSpringer Verlag
Pages321-336
Number of pages16
ISBN (Print)9783540578673
Publication statusPublished - 1 Jan 1994
Event9th Workshop on Specification of Abstract Data Types joint with 4th COMPASS Workshop, 1992 - Caldes de Malavella, Spain
Duration: 26 Oct 199230 Oct 1992

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume785 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th Workshop on Specification of Abstract Data Types joint with 4th COMPASS Workshop, 1992
CountrySpain
CityCaldes de Malavella
Period26/10/9230/10/92

Fingerprint

Dive into the research topics of 'Second-order proof systems for algebraic specification languages'. Together they form a unique fingerprint.

Cite this