高阶逻辑定理证明技术

高阶逻辑广泛适用于程序验证与自然语言语义描述，本项目基于广义配合方法和连接方法扩同阶逻辑定理证明技术，创造出新的定理证明技术—基于配对方法的高阶逻辑定理证明技术，实现了高阶逻辑定理证明系统，并将该证明技术用于汉语语义表达式的化简和异构同义的等价性证明，这是本课题组人员关于汉语计算语义理论专题研究中的一个重要组成部分，是国内外在此方向上的首次尝试，其框架结构已获得国内汉语语言学家和计算计算语言学家的高度赞赏。本项目的研究成果将继续用于描述汉语虚词语义的高阶模态逻辑系统，并最终实现汉语语义表达式的自动生成和计算。