Text this: A many-sorted calculus based on resolution and paramodulation /