 Many-sorted logic provides a semantical concept of consequence as well as a deductive calculus to be used in the mathematical process of obtaining conclusions from hypotheses. Now the issue is to automate this reasoning process by building a computer program to conduct deductive inferences.