首页> 中国专利> 一阶逻辑中基于扩展三角形的矛盾体分离演绎推理方法

一阶逻辑中基于扩展三角形的矛盾体分离演绎推理方法

摘要

本发明公开了一阶逻辑中基于扩展三角形的矛盾体分离演绎推理方法,该方法依次通过:对于一阶逻辑中的子句集构造扩展三角形标准矛盾体,形成标准矛盾体分离式,根据标准矛盾体分离式判断子句集的不可满足性;如果能够判断子句集不可满足,则停止得到结论:被判定的子句集S不可满足;否则,将所得标准矛盾体分离式加入子句集S,形成新的子句集,然后重复构造扩展三角形标准矛盾体,并分离扩展三角形标准矛盾体,直至得到子句集S属性的判定结论或满足设定条件停止;本发明提供了一阶逻辑中一种有效的基于矛盾体分离的动态自动演绎推理方法,能有效刻画多个子句间的协同逻辑关系,并可应用于程序验证、定理机器证明等领域。

著录项

  • 公开/公告号CN108875945A

    专利类型发明专利

  • 公开/公告日2018-11-23

    原文格式PDF

  • 申请/专利权人 西南交通大学;

    申请/专利号CN201710335328.2

  • 申请日2017-05-12

  • 分类号

  • 代理机构成都天嘉专利事务所(普通合伙);

  • 代理人蒋斯琪

  • 地址 610031 四川省成都市金牛区二环路北一段111号

  • 入库时间 2023-06-19 07:20:09

法律信息

  • 法律状态公告日

    法律状态信息

    法律状态

  • 2018-12-18

    实质审查的生效 IPC(主分类):G06N5/04 申请日:20170512

    实质审查的生效

  • 2018-11-23

    公开

    公开

相似文献

  • 专利
  • 中文文献
  • 外文文献
获取专利

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号