如何证明一种证明搜索方法不是另一种方法的实例
计算机科学中的逻辑
2023-04-25 v1
摘要
我们引入一种方法来证明一种证明搜索方法不是另一种方法的实例。作为应用示例，我们证明 Polarized resolution modulo（一种混合了子句选择限制与文字选择限制的方法）不是带选择的序分辨率（Ordered resolution with selection）的实例。
引用
@article{arxiv.2304.11882,
title = {How can we prove that a proof search method is not an instance of another?},
author = {Guillaume Burel and Gilles Dowek},
journal= {arXiv preprint arXiv:2304.11882},
year = {2023}
}