一阶定理证明中的包含消解
计算机科学中的逻辑
2020-01-29 v1
摘要
受一阶定理证明在软件分析中应用的推动，我们引入了一种新的推理规则，称为包含消解（subsumption demodulation），以改进基于超位置演算的定理证明中对带条件等式推理的支持。我们证明了包含消解是一种简化规则，不需要对底层超位置演算进行根本性改变。我们在定理证明器 Vampire 中实现了包含消解，通过为 Vampire 扩展新的子句索引并调整其多文字匹配组件。我们使用 TPTP 和 SMT-LIB 仓库进行的实验表明，Vampire 中的包含消解可以解决许多迄今为止最先进推理器无法解决的新问题。
引用
@article{arxiv.2001.10213,
title = {Subsumption Demodulation in First-Order Theorem Proving},
author = {Bernhard Gleiss and Laura Kovacs and Jakob Rath},
journal= {arXiv preprint arXiv:2001.10213},
year = {2020}
}