A MANY-SORTED CALCULUS BASED ON RESOLUTION AND PARAMODULATION - Walther, Christoph
Keywords: Automatic Theorem Proving