• 主题
高级搜索  >
历史搜索 清空历史
首页> 美国政府科技报告 >Theory of Adaptive Mechanisms. Part Iii. Efficient Maximal Semantic Resolution Proofs Based Upon Binary Semantic Trees
【24h】

Theory of Adaptive Mechanisms. Part Iii. Efficient Maximal Semantic Resolution Proofs Based Upon Binary Semantic Trees

机译：自适应机制理论。第一部分。基于二进制语义树的高效最大语义分辨率证明

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

A new proof procedure is presented which generates an efficient maximal semantic resolution proof of the inconsistency of any wff (well formed formula) of first order logic without equality. This is done by constructing one path at a time down a binary semantic tree. The new proof procedure has the parameters: any model for the wff and any total ordering of the Herbrand base of the wff. This technique is more efficient than the method of inference nodes because more powerful inferences are made and the path need not be constructed to the bottom of the binary semantic tree for a resolution to be performed. It is also more efficient than the British Museum Algorithm for maximal semantic resolution. For a propositional wff, it is shown that the prime implicants can be generated by repeated applications of binary resolution and the subsumption rule. Furthermore, the prime implicants which cover a particular model (i.e., a zero-cube on the Karnaugh map) can be efficiently generated by repeated applications of maximal semantic resolution and the subsumption rule. (Author)

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号