Set Theory, Higher Order Logic or Both?
Set Theory, Higher Order Logic or Both?
复制标题
集合论、高阶逻辑或两者兼而有之？
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
M. Gordon
中科院分区：
文献类型：
--
作者：
M. Gordon
尽管集合论是数学的标准基础，但大多数通用的机械化证明助手支持类型化高阶逻辑的版本。对于许多应用程序，高阶逻辑工作良好，并提供了规范，类型检查的好处，这是众所周知的编程。然而，在某些领域，类型会妨碍或似乎没有动力。此外，大多数具有科学或工程背景的人已经知道集合论，但不知道高阶逻辑。本文讨论了两全其美的一些方法：集合论的表达性和标准性与类型化高阶逻辑提供的函数的有效处理。
The majority of general purpose mechanised proof assistants support versions of typed higher order logic, even though set theory is the standard foundation for mathematics. For many applications higher order logic works well and provides, for specification, the benefits of type-checking that are well-known in programming. However, there are areas where types get in the way or seem unmotivated. Furthermore, most people with a scientific or engineering background already know set theory, but not higher order logic. This paper discusses some approaches to getting the best of both worlds: the expressiveness and standardness of set theory with the efficient treatment of functions provided by typed higher order logic.