Universal Abstract Consistency Class and Universal Refutation

Refutation methods based on the resolution principle are generally applied to a (finite) set of sentences, which must have a series of pre-transformations (prenex normalization, Skolemization and conjunction normalization) before starting the refutation. In this paper, the authors first generalize the concept of abatract consistency class to the most general form-universal abstract consistency class, and prove its universal unifying principle. Then, based on the R-refutation, a universal refutation method i…