The Ontological Argument in PVS
The Ontological Argument in PVS
复制标题
PVS 中的本体论论证
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
J. Rushby
中科院分区：
文献类型：
--
作者：
J. Rushby
本体论论证是11世纪对上帝存在的证明，是《形式化方法的乐趣》的一个很好的候选，因为几乎每个人都觉得这个话题很有趣。我们在PVS中形式化了实参，并验证了其正确性。形式化在形式逻辑中提出了一些微妙的问题，并提供了一个机会来展示如何通过PVS的预测性子类型高阶逻辑及其机械化支持来合理有效地处理这些问题。论证的简单性，加上其大胆的结论，对现实世界中形式方法的解释和应用提出了有趣的问题。
The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in PVS and verify its correctness. The formalization raises delicate questions in formal logic and provides an opportunity to show how these are handled, soundly and efficiently, by the predicatively-subtyped higher-order logic of PVS and its mechanized support. The simplicity of the Argument, coupled to its bold conclusion, raise interesting issues on the interpretation and application of formal methods in the real world.