Theorem Proving; Logic Programming

T-resolution parametrically generalizes standard resolution with respect to a first-order theory T (the parameter). The inherent power of its derivation rule, however, makes it difficult to develop efficient unrestricted T -resolution based systems. …