||Diagrammatic Calculus for Order-sorted Logic
寺川, 宏之 ,
吉岡, 卓 ,
TERAKAWA, HiroyukiYOSHIOKA, Suguru
42 , 2018-03-01 , 都留文科大学
In the field of artificial intelligence, order-sorted logics, that have subsumptionrelations 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. Inordinary cases, such subsumption relations organizes a lattice, the operations of ‘join’ and‘meet’ being assumed. However, in dual systems, the description of two different latticesof predicates and sorts, makes us hard to find reasonability between atomic formulae. Inthis paper, we propose a representation of cellular table for the dual hierarchies, assigninga Gödel number to each node to identify its spacial position. Thus, we can describe twolattices in one table, and in addition, the reasonability between two atomic formulae isreduced to simple numerical calculation. Therefore, (i) the reasonability between twodistant atomic formulae and (ii) the scope of partial negation are easily displayed, and inaddition, (iii) that the whole table is adequately maintained even in case new subsumptionrelations are added. We implemented a deduction system on a computer, and showed itsefficiency.