基于类型一阶理论的逻辑自动编程

摘要

本文用类型一阶理论来定义逻辑程序，并通过引入Ｌａｋａｔｏｓ的基于证伪的发现方法论将原有的封闭型类型一阶理论改造为开放的类型一阶理论，在此基础上，建立了一个基于假说演算的逻辑自动程编程理论，并利用这一理论在Ｓｕｎ工作站上建立了一个自动设计Ｐｒｏｌｏｇ型程序的实验系统。