Higher Order Unification and Mechanization of Higher Order Theorem Proving System

点击翻译按钮获取中文摘要

We have studied in this year by setting the following themes : (1) Formalization of higher order logic language based on lambda-logic, (2) Design of higher order unification algorithm for mechanizing theorem proving system, (3) Higher order inference system for knowledge processings.For the theme (1), we designed a higher order program language by extending the Horn clause to a higher order case, and some results have been obtained. For the theme (2), a new class of higher order language in which the unification algorithm becomes computable has been made clear. Especially computational complexity of unification algorithm for 2nd order terms has been discussed precisely. For (3), we have demonstrated that a kind of analogical reasoning system can be realized in the framework of proposed higher order language, and it is ascertained that the proposed method is available for designing intelligent knowledge processing system.