新论文:“HOL的打样反思”

||论文

假日MIRI研金宝博娱乐究员Benya Fallenstein和研究助理Ramana Kumar合著了一篇关于机器反射的新论文。”用一个应用程序对多态性建模的HOL的证明生成反射.”

假日代表高阶逻辑,这里指的是一种流行的举证助理的家庭基于教会的类型理论.Kumar和合作者之前在HOL (具体来说,HOL4)在HOL中什么是可证明的,成为HOL的典范意味着什么。1在“高阶逻辑的自形式化Kumar, Arthan, Myreen, Owens证明了如果在HOL中有什么是可以证明的,那么它在所有的HOL模型中都是正确的。

“为HOL打样反思”建立在这一结果的基础上,通过展示HOL内部的HOL模型(“内部的HOL”)和HOL本身(“外部的HOL”)之间的正式对应关系。非正式地说,Fallenstein和Kumar表明,人们总是可以构建一个内部HOL术语的解释,使它们具有与外部HOL术语相同的含义。然后,作者证明了某种类型的陈述是可证明的在HOL自身的模式中,他们是真正的在(外部)假日。这种通信使作者能够使用HOL来实现模型多态性,机器自我验证的方法,见《Vingean反思:自我改进代理的可靠推理.”2

这个项目的动机是这样一个事实:在正式验证系统中对正式验证系统建模的实际工作相对较少,特别是对它们本身建模的实际工作相对较少。金宝博官方Fallenstein指出,只关注Vingean反射的数学理论可能会使我们无法准确地校准软件实现的工程困难所在。在实现模型多态性的过程中,Fallenstein和Kumar确实遇到了以往理论工作中不明显的困难,其中最重要的是来自HOL多态性

Fallenstein和Kumar的论文是在2015年国际旅游业伙伴关系可以被发现在线或者在相关的会议论文集.多亏了生命未来研究所的资助,库马尔和法伦斯坦将继续他们在这个项目上的合作。在“HOL举证反思”的后续工作中,Kumar和Fallenstein的下一个目标将是开发HOL举证助手中使用模型多态性推理的代理的玩具模型。


  1. Kumar研究表明,如果HOL中存在集合理论模型,那么HOL中也存在一个HOL模型。此外,Fallenstein和Kumar还表明,如果一个更简单的公理成立,HOL中存在一个集合理论模型。
  2. 更多关于逻辑推理在机器反射中的作用,请参阅Fallenstein的2013关于自我修改系统的对话金宝博官方