关系语义学的一个证明理论基础
A proof theoretic basis for relational semantics
摘要：
逻辑已被证明是必不可少的正式建模软件为基础的系统。这种形式化的描述，通常被称为规范，不仅作为需求文档和形式化，而且还为它们的分析和自动推理工具的开发提供了数学基础。逻辑学通常从其内在的两个方面来研究：句法和语义。后者的相关性在于这样一个事实，即对现实世界的现象进行逻辑描述，需要人们就人类如何解释和理解这些描述达成一致，以便系统可以根据其规范自信地构建。在更实际的方面，句法和语义之间的元逻辑关系决定了人们可以从某些分析技术的应用中得出的结论的重要方面，如模型检验。抽象模型理论（Abstract Model Theory）关于逻辑语言语义的数学观点）对于软件工程努力几乎没有实用价值。从我们的观点来看，值（可以分配给常量和变量的值）不应该仅仅是柏拉图式解释域中的点，而是可以通过规范签名上的术语命名的元素。简而言之，我们对那些需要任何语义信息而无法用可用语法表示的属性不感兴趣。在本文中，我们提出了一个框架，支持证明理论的形式化类的关系模型的行为逻辑语言，其域的话语保证只形成命名值。
英文摘要：
Logic has proved essential for formally modeling software based systems. Such formal descriptions, frequently called specifications, have served not only as requirements documentation and formalisation, but also for providing the mathematical foundations for their analysis and the development of automated reasoning tools. Logic is usually studied in terms of its two inherent aspects: syntax and semantics. The relevance of the latter resides in the fact that producing logical descriptions of real-world phenomena, requires people to agree on how such descriptions are to be interpreted and understood by human beings, so that systems can be built with confidence in accordance with their specification. On the more practical side, the metalogical relation between syntax and semantics, determines important aspects of the conclusions one can draw from the application of certain analysis techniques, like model checking. Abstract model theory (i.e., the mathematical perspective on semantics of logical languages) is of little practical value to software engineering endeavours. From our point of view, values (those that can be assigned to constants and variables) should not be just points in a platonic domain of interpretation, but elements that can be named by means of terms over the signature of the specification. In a nutshell, we are not interested in properties that require any semantic information not representable using the available syntax. In this paper we present a framework supporting the proof theoretical formalisation of classes of relational models for behavioural logical languages, whose domains of discourse are guaranteed to be formed exclusively by nameable values.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
