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来实现模型多态性第6.3节中描述的机器自验证方法。Vingean reflection:自我改进的可靠推理．”2
这个项目的动机是，在形式化验证系统中，对于形式化验证系统的建模，尤其是对形式化系统本身的建模，已经做了相对较少的实践工作。亚博体育苹果app官方下载Fallenstein指出，只关注Vingean反射的数学理论可能会使我们在软件实现的工程困难所在方面缺乏校准。在实现模型多态性的过程中，Fallenstein和Kumar确实遇到了以往理论工作中不明显的困难，其中最重要的困难来自HOL多态性．
Fallenstein和Kumar的论文发表于2015年国际旅游业伙伴关系并且可以被发现在线或者在相关的会议论文集．多亏了由生命未来研究所资助库马尔和法伦斯坦将继续在这个项目上合作。继“HOL的证明生产反射”之后，Kumar和Fallenstein的下一个目标将是在HOL证明助手中开发使用模型多态性推理的代理玩具模型。
- Kumar证明，如果在HOL中存在集合理论模型，那么在HOL中就存在HOL模型。Fallenstein和Kumar还指出，如果一个更简单的公理成立，那么HOL中存在一个集合理论的模型。↩
- 更多关于逻辑推理在机器反射中的作用，参见Fallenstein的2013年关于自我修正系统的对话亚博体育苹果app官方下载．↩
