Introducing Institutions
Introducing Institutions
复制标题
机构介绍
DOI：
--
复制
发表时间：
1983
期刊：
影响因子：
--
通讯作者：
R. Burstall
中科院分区：
文献类型：
--
作者：
J. Goguen;R. Burstall
在计算机科学中使用的逻辑系统之间存在人口爆炸。 ，临时逻辑和模态逻辑；对于每个逻辑系统，当然，这在计算机科学的基本结果中是自然而然的，这些结果与逻辑系统无关，但我们不必一遍又一遍。同样，我们应该概括一下，一劳永逸！合适的逻辑系统，通过将ins t i t t ion的概念作为对胎体系统的非正式通知的精确概括，第一个主要结果表明，如果机构是这样表达的界面声明，则可以粘合在一起，然后在该机构中的理论（仅是一组句子）也可以粘合在一起机构形态的概念。并包括所谓的•数据，”“层次结构，•和再生”的约束。进一步的结果显示了如何定义从一个机构中将句子与约束的注射句子。另一个，甚至混合了几个不同机构的句子和{各种）约束。这些结果是指规语言，表明该主题的大部分实际上与所使用的机构无关。
There is a population explosion among the logical systems being used in computer science. Examples include first order logic (with and without equality), equational logic, Horn clause logic, second order logic, higher order logic, infinitary logic, dynamic logic, process logic, temporal logic, and modal logic; moreover ~, there is a tendency for each theorem prover to have its own idiosyncratic logical system. Yet it is usual to give many of the same results and applications for each logical system; of course, this is natural in so far as there are basic results in computer science that are independent of the logical system in which they happen to be expressed. But we should not have to do the same things over and over again; instead, we should generalize, and do the essential things once and for all! Also, we should ask what are the relationships among all these different logical systems. This paper shows how some parts of computer science can be done in any suitable logical system, by introducing the notion of an ins t i tu t ion as a precise generalization of the informal notion of a mlogical system, m A first main result shows that if an institution is such that interface declarations expressed in it can be glued together, then theories {which are just sets of sentences) in that institution can also be glued together. A second main result gives conditions under which a theorem prover for one institution can be validly used on theories from another; this uses the notion of an institution morphism. A third main result shows that institutions admiting free models can be extended to institutions whose theories may include, in addition to the original sentences, various kinds of constraints upon interpretations; such constraints are useful for defining abstract data types, and include so-called • data," "hierarchy, • and regenerating" constraints. Further results show how to define insitutions that mix sentences from one institution with constraints from another, and even mix sentences and {various kinds of) constraints from several different institutions. It is noted that general results about institutions apply to such mmultiplex" institutions, including the result mentioned above about gluing together theories. Finally, this paper discusses some applications of these results to specification languages, showing that much of that subject is in fact independent of the institution used.