Extensions of initial models and their second-order proof systems

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

Abstract

Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as initiality. For proving properties of specifications and refining them to programs, an axiomatization of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for initial models, and a fortiori for their extensions. In this paper, we construct non-effective second-order axiomatizations for the initiality constraint, and its recently proposed extensions (minimal, quasi-free and surjective models) designed to deal with disjunction and existential quantification.

Original languageEnglish
Title of host publicationHigher-Order Algebra, Logic, and Term Rewriting - 1st International Workshop, HOA 1993, Selected Papers
PublisherSpringer Verlag
Pages326-344
Number of pages19
ISBN (Print)9783540582335
Publication statusPublished - 1 Jan 1994
Event1st International Workshop on Higher-Order Algebra,Logic and Term Rewriting, HOA 1993 - Amsterdam, Netherlands
Duration: 23 Sep 199324 Sep 1993

Publication series

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

Conference

Conference1st International Workshop on Higher-Order Algebra,Logic and Term Rewriting, HOA 1993
CountryNetherlands
CityAmsterdam
Period23/09/9324/09/93

Fingerprint

Dive into the research topics of 'Extensions of initial models and their second-order proof systems'. Together they form a unique fingerprint.

Cite this