Extensions of initial models and their second-order proof systems

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 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.

langue originaleAnglais
titreHigher-Order Algebra, Logic, and Term Rewriting - 1st International Workshop, HOA 1993, Selected Papers
EditeurSpringer Verlag
Pages326-344
Nombre de pages19
ISBN (imprimé)9783540582335
Etat de la publicationPublié - 1 janv. 1994
Evénement1st International Workshop on Higher-Order Algebra,Logic and Term Rewriting, HOA 1993 - Amsterdam, Pays-Bas
Durée: 23 sept. 199324 sept. 1993

Série de publications

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

Une conférence

Une conférence1st International Workshop on Higher-Order Algebra,Logic and Term Rewriting, HOA 1993
Pays/TerritoirePays-Bas
La villeAmsterdam
période23/09/9324/09/93

Empreinte digitale

Examiner les sujets de recherche de « Extensions of initial models and their second-order proof systems ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation