Diagrammatic Calculus for Order-sorted Logic

Abstract

In the field of artificial intelligence, order-sorted logics, that have subsumption relations between sorts, are widely utilized for structural knowledge representations. Among them, dual hierarchical systems, that have subsumption relations also in events (predicates) as well as sorts (terms), can realize superb efficiency in logical reasoning. In ordinary cases, such subsumption relations organizes a lattice, the operations of ‘join’ and ‘meet’ being assumed. However, in dual systems, the description of two different lattices of predicates and sorts, makes us hard to find reasonability between atomic formulae. In this paper, we propose a representation of cellular table for the dual hierarchies, assigning a Gödel number to each node to identify its spacial position. Thus, we can describe two lattices in one table, and in addition, the reasonability between two atomic formulae is reduced to simple numerical calculation. Therefore, (i) the reasonability between two distant atomic formulae and (ii) the scope of partial negation are easily displayed, and in addition, (iii) that the whole table is adequately maintained even in case new subsumption relations are added. We implemented a deduction system on a computer, and showed its efficiency.