TY - GEN
T1 - Extensions of initial models and their second-order proof systems
AU - Schobbens, Pierre Yves
PY - 1994/1/1
Y1 - 1994/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85028805567&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85028805567
SN - 9783540582335
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 326
EP - 344
BT - Higher-Order Algebra, Logic, and Term Rewriting - 1st International Workshop, HOA 1993, Selected Papers
PB - Springer Verlag
T2 - 1st International Workshop on Higher-Order Algebra,Logic and Term Rewriting, HOA 1993
Y2 - 23 September 1993 through 24 September 1993
ER -