Item

Abstract

We present a sound and complete calculus $\cal {CL}_S$ for the first-order logic ${\cal L_S}$ without equality but dynamic sorts. By dynamic sorts we understand a sort structure which is exploited during the deduction process and is not fixed from the beginning. Therefore the logic allows arbitrary sort declarations and every first-order logic formula can be compiled into our logic. Deductions in the calculus turn out to be very efficient as will be shown by examples. Thus the new logic signifacantly improves the efficiency of automated deductions if one-place predicates (sorts) are involved in the reasoning process. Furthermore the calculus $\cal {CL}_S$ is conservative extension of the existing approaches to sorted logic. That means if the sorted information could be represented in the known approaches the more general calculus $\cal {CL}_S$ has the same behaviour as the existing calculi.