首页> 外国专利> METHOD OF AUTOMATED PROVING FOR UNRESTRICTED FIRST-ORDER LOGIC

METHOD OF AUTOMATED PROVING FOR UNRESTRICTED FIRST-ORDER LOGIC

机译:无约束一阶逻辑的自动证明方法

摘要

The method of automated proving for unrestrictedfirst-logic to test the satisfiability of clause sets describingan industrial system applies the instance generation rule(IG)~~~.sigma.where ~ is a term, .sigma. a substitution and ~.sigma. an instance of ~yielded by the substitution .sigma., and is characterized in that,defining an instance subtraction as the subtraction of theinstance ~.sigma. from ~ resulting in a generalized term which isa triplet ~, .sigma., ~ where ~ is a finite set of standardsubstitutions {.lambda.1, ..., .lambda.n} and defined byGE(~, .sigma., ~) = GE (~.sigma.)~ - GE ({~.lambda.1, ..., ~.lambda.n})the method further applies an instance subtraction combinedwith said instance generation rule to get an instanceextraction rule defined by(IE) .SIGMA. ~ (.SIGMA. - {~.sigma.,~})~{~.sigma.µ, ~*.sigma.µ,~.sigma., ~~{.sigma.µ})where .SIGMA. is a set of clauses and µ is a substitution validfor the generalized term ~.sigma., ~, whereby the set .SIGMA. can beproved unsatisfiable.
机译:无限制自动证明的方法测试子句集描述的可满足性的第一逻辑工业系统应用实例生成规则(IG)~~〜.sigma。〜是一个术语,.sigma。替换和〜.sigma。 〜的一个实例由替换σ产生,其特征在于,将实例减法定义为实例〜.sigma。从〜得到一个广义项,即三元组<〜,.sigma。,〜>,其中〜是一组有限的标准替换{.lambda.1,...,.lambda.n}并定义为GE(<〜,.sigma。,〜>)= GE(〜.sigma。)〜-GE({〜.lambda.1,...,〜.lambda.n})该方法进一步应用实例减法组合用所述实例生成规则来获取实例提取规则定义为(IE).SIGMA。 〜(.SIGMA。-{〜<.sigma。,〜>})〜{〜<.sigma.µ,〜* .sigma.µ>,〜<.sigma。,~~ {.sigma.µ}>).SIGMA。是一组子句,µ是替代有效对于广义项〜<.sigma。,〜>,从而设置.SIGMA。可证明是不满意的。

著录项

  • 公开/公告号CA2133699C

    专利类型

  • 公开/公告日1999-09-07

    原文格式PDF

  • 申请/专利权人

    申请/专利号CA19942133699

  • 发明设计人 BILLON JEAN-PAUL;

    申请日1994-10-05

  • 分类号G06F9/44;G06F15/18;

  • 国家 CA

  • 入库时间 2022-08-22 02:24:09

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号