Vampire与FOOL
计算机科学中的逻辑
2015-12-08 v2
摘要
本文介绍了近期在定理证明器Vampire中实现的新特性，即对带有一等布尔排序的一阶逻辑(FOOL)和多态数组的支持。除了具有一等布尔排序外，FOOL还包含if-then-else和let-in表达式。我们认为所提出的扩展促进了基于推理的程序分析，既通过提高一阶推理器的表达能力，也通过效率的提升。
引用
@article{arxiv.1510.04821,
title = {The Vampire and the FOOL},
author = {Evgenii Kotelnikov and Laura Kovács and Giles Reger and Andrei Voronkov},
journal= {arXiv preprint arXiv:1510.04821},
year = {2015}
}