一种一阶并行、带优先级和逐点的限定理论计算方法

专利申请号：CN201510097186.1

公 开 号：CN104750974A

发 明 人：万海 萧展豪 曾娟 

代 理 人：林丽明

代理机构：44102 广州粤高专利商标代理有限公司

专利类型：发明申请

申 请 日：20150701

公 开 日：20150304

专利主分类号：G06F19/00(20110101)

关 键 词：优先级 求解器 量词 理论计算方法 设计与实现 在线性时间 语义 高效计算 逻辑等价 优化翻译 优化算法 算法 谓词 语法 辅助 层面 

摘      要：本发明公开一种一阶并行、带优先级和逐点的限定理论计算方法，包括：（1）将任意一个一阶限定理论在线性时间内翻译为另一个与之在任意结构上逻辑等价的在稳定语义下的一阶理论，包括四个基于语法层面的主要翻译；（2）对于一阶限定理论中的存在量词，提出了消去存在量词的优化翻译算法，该方法不仅减少了引入的辅助谓词数量，而且减少了由翻译造成的理论的规模的增长；（3）基于以上的翻译和消去存在量词优化算法，本发明实现了一个能够在给定的论域中求出所有极小模型的通用一阶限定理论求解器。本发明解决了一阶并行、带优先级和逐点的限定理论缺乏的求解器的现状，可以设计与实现可高效计算的一阶并行、带优先级和逐点的限定理论求解器。