How can we prove that a proof search method is not an instance of another?
Logic in Computer Science
2023-04-25 v1
Abstract
We introduce a method to prove that a proof search method is not an instance of another. As an example of application, we show that Polarized resolution modulo, a method that mixes clause selection restrictions and literal selection restrictions, is not an instance of Ordered resolution with selection.
Keywords
Cite
@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}
}