Structuring Metatheory on Inductive Definitions
Structuring Metatheory on Inductive Definitions
复制标题
构建归纳定义的元理论
DOI：
10.1006/inco.2000.2858
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
S. Matthews
中科院分区：
文献类型：
--
作者：
D. Basin;S. Matthews
我们研究一个问题，机器支持的元理论。有一些关于一个理论的真陈述对某些（但只有某些）扩展是真的;然而，标准的理论结构工具不支持选择性继承。我们使用模态逻辑的演绎定理的例子，并显示如何一个理论的声明可以明确形式化的封闭条件扩展应该满足它保持真实。我们展示了如何元理论的基础上归纳定义允许理论和一般元定理组织这种方式和报告的案例研究使用的理论FS 0。
We examine a problem for machine supported metatheory. There are true statements about a theory that are true of some (but only some) extensions; however, standard theory-structuring facilities do not support selective inheritance. We use the example of the deduction theorem for modal logic and show how a statement about a theory can explicitly formalize the closure conditions extensions should satisfy for it to remain true. We show how metatheories based on inductive definitions allow theories and general metatheorems to be organized this way and report on a case study using the theory FS0.