...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >Decomposable theories
【24h】

Decomposable theories

机译：可分解理论

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

摘要

We present in this paper a general algorithm for solving first-order formulas in particular theories called decomposable theories. First of all, using special quantifiers, we give a formal characterization of decomposable theories and show some of their properties. Then, we present a general algorithm for solving first-order formulas in any decomposable theory T. The algorithm is given in the form of five rewriting rules. It transforms a first-order formula φ, which can possibly contain free variables, into a conjunction Φ of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if φ has no free variables then Φ is either the formula true or -true. The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory I of finite or infinite trees is a decomposable theory and give some benchmarks realized by an implementation of our algorithm, solving formulas on two-partner games in J with more than 160 nested alternated quantifiers.
机译：我们在本文中提出了一种用于求解一阶公式的通用算法，特别是称为可分解理论的特定理论。首先，使用特殊的量词，我们对可分解理论进行了形式化表征，并展示了它们的一些特性。然后，我们提出了一种求解任何可分解理论T中一阶公式的通用算法。该算法以五个重写规则的形式给出。它将可能包含自由变量的一阶公式转换为可轻松转换为原子公式的存在性量化合取的布尔组合的已求解公式的合取Φ。特别是，如果φ没有自由变量，则φ可以是公式true或-true。我们算法的正确性证明了可分解理论的完整性。最后，我们证明了有限树或无限树的理论I是可分解的理论，并给出了通过实施我们的算法实现的一些基准，并用超过160个嵌套的交替量词求解了J中两伙伴游戏的公式。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号