Proving the completeness of theory-based variants of resolution