Text this: The resolution calculus