Polarized Resolution Modulo

Abstract. We present a restriction of Resolution modulo where the rewrite rules are such that a clause always rewrites to a clause. This way, the reduct of a clause needs not be further transformed into clause form. Restricting Resolution modulo this way requires to extend it in another way and distinguish the rules that apply to negative and to positive atomic propositions. As an example, we show how this method applies to a first-order presentation of Simple type theory. Finally, we show that this method can be seen as a restriction of Equational resolution that mixes clause selection restrictions and literal selection restrictions, but unlike many restrictions of Resolution, it is not an instance of Ordered resolution. 1