A more expressive formulation of many sorted logic (Q1101261)

In ordinary first order logic, simple facts may acquire long representing formulas; partially responsible is the lack of sortal information about objects and predicates. Consequently, many sorted logic is a tool to achieve more compact representations of knowledge in AI and to reduce the search space in automated deduction. In this paper, the author introduces a many sorted logic, which he calls LLAMA (at least the name ``logic lacking a meaningful acronym'' should not be taken serious). The basic concepts are sorting domains and sorting functions. Sorts are represented by the Boolean lattice of the set of subsets of sort symbols. Sorting functions serve to assign sorts to function- and predicate symbols; several alternatives to define sorting functions for logical connectives (particularly for \(\vee)\) are presented. Formally, there is some similarity to 4-valued logic, because besides TRUE and FALSE we have the values ``either true or false'' and ``nonsense'' (however, these are sort values, not truth values). A key notion is the concept of sort array, which is a tool to assign sorts to formulas. By associating a sort array with a formula F, one gets the sort of F in a sortal environment \((= assignment\) of sorts to variables); an algorithm to determine the sort of formulas in a sortal environment is given. Semantics for LLAMA is defined formally and many sorted inference rules are introduced, among them many sorted resolution for clausal forms. Finally, the author gives a detailed comparison with other approaches, particularly with that off \textit{C. Walther} [A many sorted calculus based on resolution and paramodulation, Proc. IJCAI-83, Karlsruhe, William Kaufmann, 882-899 (1983; for a general review of these proceedings see Zbl 0536.68074)]. The example of ``Schubert's steamroller'' is used to demonstrate the strong power of LLAMA; the problem is represented by 3 clauses only (compared with 27 in ordinary first order logic and 12 in Walther's logic).