Integrating Static and Dynamic Sort Checking in Logic Programming

In this paper, we first discuss the motivation and concept of a new sorting approach, called soft sorting, which combines some good features of languages using syntactic well-sortedness rules and of languages using sort predicates. We then describe an application of soft sorting approach to overcome some limitations of sorted logic programming. Keywords: Types and sorts, logic programming, static and dynamic type checking 1 Introduction of Soft Sorting When a language refers to a universe of discourse which contains more than one sort of object, it is often useful for the language to include notations for describing sort restrictions on functions and predicates so as to achieve more flexible representations and more efficient reasoning. Increased efficiency is typically based on sort restrictions, which may be checked either statically or dynamically. Languages using syntactic sort constraints ("signatures") on function and relation symbols support more static sort checking but are le..