Comprehending Isabelle/HOL's Consistency
Comprehending Isabelle/HOL's Consistency
复制标题
理解 Isabelle/HOL 的一致性
DOI：
10.1007/978-3-662-54434-1_27
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Andrei Popescu
中科院分区：
文献类型：
--
作者：
Ondřej Kunčar;Andrei Popescu
证明助手Isabelle/HOL是基于高阶逻辑（HOL）的扩展，具有常量的特设重载。事实证明，标准HOL类型定义和Isabelle特定的特殊重载之间的交互对于逻辑一致性来说是有问题的。在以前的工作中，我们认为，标准的HOL语义不再适合捕捉这种相互作用，并证明了使用非标准语义的一致性。使用外来语义使得社区难以理解该证明。在本文中，我们证明了一致性的证明理论的手段，以下健康的直觉定义的缩写，实现在HOLC，逻辑，增强HOL的理解类型。我们希望我们的新证明一劳永逸地解决了Isabelle/HOL一致性问题。此外，HOLC提供了一个框架，证明新的演绎模式，解决实际用户的需求的一致性。
The proof assistant Isabelle/HOL is based on an extension of Higher-Order Logic (HOL) with ad hoc overloading of constants. It turns out that the interaction between the standard HOL type definitions and the Isabelle-specific ad hoc overloading is problematic for the logical consistency. In previous work, we have argued that standard HOL semantics is no longer appropriate for capturing this interaction, and have proved consistency using a nonstandard semantics. The use of an exotic semantics makes that proof hard to digest by the community. In this paper, we prove consistency by proof-theoretic means—following the healthy intuition of definitions as abbreviations, realized in HOLC, a logic that augments HOL with comprehension types. We hope that our new proof settles the Isabelle/HOL consistency problem once and for all. In addition, HOLC offers a framework for justifying the consistency of new deduction schemas that address practical user needs.
登录
查看更多内容
DOI：
10.1007/11805618_16
发表时间：
2006
期刊：
Arch. Formal Proofs
影响因子：
--
作者：
Steven Obua
通讯作者：
Steven Obua
DOI：
10.1007/978-3-319-08867-9_11
发表时间：
2014
期刊：
18th IEEE Computer Security Foundations Workshop (CSFW'05)
影响因子：
--
作者：
Sudeep Kanav;P. Lammich;A. Popescu
通讯作者：
A. Popescu
Coq 中的集合，Coq 中的集合
DOI：
10.6092/issn.1972-5787/1695
发表时间：
2010
期刊：
J. Formaliz. Reason.
影响因子：
--
作者：
Bruno Barras
通讯作者：
Bruno Barras
通过类型变量的量化扩展 HOL 逻辑
影响因子：
0.8
作者：
T. Melham
通讯作者：
T. Melham
Isabelle/HOL 的一致基础
DOI：
10.1007/s10817-018-9454-8
发表时间：
2015
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Ondrej Kuncar;A. Popescu
通讯作者：
A. Popescu