A MANY-SORTED NATURAL DEDUCTION

The goal of this paper is to motivate and define yet another sorted lo gic, called SND. All the previous sorted logics that can he found in t he Artificial Intelligence literature have been designed to be used in (completely) automated deduction. SND has been designed to be used in interactive theorem proving. Because of this shift of focus, SND has been designed to satisfy three innovative design requirements: it is d efined on top of a natural deduction calculus, and in a way to be a de finitional extension of such calculus; and it is implemented on top of its implementation. In turn, because of this fact, SND has various in novative technical properties; among them: it allows us to deal with f ree variables, it has no notion of well-sortedness and of well-sortedn ess being a prerequisite of well-formedness, its implementation is suc h that, in the default mode, the system behaves exactly as with the or iginal unsorted calculus.