The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning

摘要

Researchers in artificial intelligence have recently been taking great interest in hybrid representations, among them sorted logics—logics that link a traditional logical representation to a taxonomic (or sort) representation such as those prevalent in semantic networks. This paper introduces a general framework—the substitutional framework—for integrating logical deduction and sortal deduction to form a deductive system for sorted logic. This paper also presents results that provide the theoretical under-pinnings of the framework. A distinguishing characteristic of a deductive system that is structured according to the substitutional framework is that the sort subsystem is invoked only when the logic subsystem performs unification, and thus sort information is used only in determining what substitutions to make for variables. Unlike every other known approach to sorted deduction, the substitutional framework provides for a systematic transformation of unsorted deductive systems into sorted ones.