Aug, 2020

使用Anthem和Vampire验证紧凑逻辑程序

TL;DR研究逻辑程序与一阶理论之间关系的论文,将程序完备性的定义扩展到具有一种程序翻译器中输入语言子集的输入和输出程序,研究了这种情况下稳定模型和完备性之间的关系,并描述了两个软件工具,anthem 和 vampire,用于验证具有输入和输出的程序的正确性。