...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Annals of Mathematics and Artificial Intelligence >A new algebraic tool for Automatic Theorem Provers Multisemilattice: A structure to improve the efficiency of provers in temporal logics
【24h】

A new algebraic tool for Automatic Theorem Provers Multisemilattice: A structure to improve the efficiency of provers in temporal logics

机译：自动定理证明多重半精算的新代数工具：一种提高时间逻辑证明者效率的结构

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The concepts of implicates and implicants are widely used in several fields of "Automated Reasoning". Particularly, our research group has developed several techniques that allow us to reduce efficiently the size of the input, and therefore the complexity of the problem. These techniques are based on obtaining and using implicit information that is collected in terms of unitary implicates and implicants. Thus, we require efficient algorithms to calculate them. In classical propositional logic it is easy to obtain efficient algorithms to calculate the set of unitary implicants and implicates of a formula. In temporal logics, contrary to what we see in classical propositional logic, these sets may contain infinitely many members. Thus, in order to calculate them in an efficient way, we have to base the calculation on the theoretical study of how these sets behave. Such a study reveals the need to make a generalization of Lattice Theory, which is very important in "Computational Algebra". In this paper we introduce the multisemilattice structure as a generalization of the semilattice structure. Such a structure is proposed as a particular type of poset. Subsequently, we offer an equivalent algebraic characterization based on non-deterministic operators and with a weakly associative property. We also show that from the structure of multisemilattice we can obtain an algebraic characterization of the multilattice structure. This paper concludes by showing the relevance of the multisemilattice structure in the design of algorithms aimed at calculating unitary implicates and implicants in temporal logics. Concretely, we show that it is possible to design efficient algorithms to calculate the unitary implicants/implicates only if the unitary formulae set has the multisemilattice structure.
机译：牵连和暗示的概念在“自动推理”的多个领域中得到了广泛使用。特别是，我们的研究小组开发了几种技术，可以使我们有效地减少输入的大小，从而减少问题的复杂性。这些技术基于获取和使用隐式信息，这些信息是根据单一含义和暗示来收集的。因此，我们需要有效的算法来计算它们。在经典命题逻辑中，很容易获得有效的算法来计算the蕴涵和公式的蕴涵集。在时间逻辑中，与我们在经典命题逻辑中看到的相反，这些集合可能包含无限多个成员。因此，为了高效地计算它们，我们必须将计算基于这些集合的行为的理论研究。这样的研究表明有必要对格子理论进行概括，这在“计算代数”中非常重要。在本文中，我们介绍了多半格结构作为半格结构的推广。提出了这样的结构作为特定类型的摆放器。随后，我们基于非确定性运算符并具有弱关联性质提供了等效的代数表征。我们还表明，从多半格的结构中，我们可以获得多格结构的代数表征。本文的结论是通过显示多半子句结构在旨在计算时间逻辑中的unit和蕴涵的算法设计中的相关性。具体而言，我们表明，只有当formula式集具有多重符号结构时，才有可能设计出有效的算法来计算the蕴涵/蕴涵。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号