Model-Theoretic Conservative Extension for Definitional Theories
Model-Theoretic Conservative Extension for Definitional Theories
复制标题
定义理论的模型理论保守扩展
DOI：
10.1016/j.entcs.2018.10.009
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Tjark Weber
中科院分区：
文献类型：
--
作者：
A. Gengelbach;Tjark Weber
许多逻辑框架允许扩展，即通过定义引入新的符号。与断言任意的非逻辑公理不同，通过定义的扩展被期望是保守的：它们不应该在原始语言中引入新的定理。流行的定理证明器Isabelle实现了一种高阶逻辑的变体，允许hocoverloading常量。在2015年，Kunčar和Popescu引入了定义理论，在这个逻辑中对常数和类型定义施加了非循环性条件，并表明这个条件足以使定义扩展保持一致性。我们加强和推广这一结果表明，扩展的定义理论是模型论保守的，即每一个模型的原始理论可以扩展到一个模型的扩展理论。
Many logical frameworks allow extensions, i.e. the introduction of new symbols, by definitions. Different from asserting arbitrary non-logical axioms, extensions by definitions are expected to be conservative: they should entail no new theorems in the original language. The popular theorem prover Isabelle implements a variant of higher-order logic that allowsad hocoverloading of constants. In 2015, Kunčar and Popescu introduceddefinitional theories, which impose a non-circularity condition on constant and type definitions in this logic, and showed that this condition is sufficient for definitional extensions to preserve consistency. We strengthen and generalize this result by showing that extensions of definitional theories are model-theoretic conservative, i.e. every model of the original theory can be expanded to a model of the extended theory.
Isabelle 循环检查器的正确性：证明助手中重载的可实现性
DOI：
10.1145/2676724.2693175
发表时间：
2015
期刊：
Proceedings of the 2015 Conference on Certified Programs and Proofs
影响因子：
--
作者：
Ondřej Kunčar
通讯作者：
Ondřej Kunčar
理解 Isabelle/HOL 的一致性
DOI：
10.1007/978-3-662-54434-1_27
发表时间：
2017
期刊：
影响因子：
--
作者：
Ondřej Kunčar;Andrei Popescu
通讯作者：
Andrei Popescu
HOL 和 Isabelle/HOL 中定义的安全性和保守性
影响因子：
--
作者：
Ondřej Kunčar;Andrei Popescu
通讯作者：
Andrei Popescu