...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Theory and Practice of Logic Programming >Transition systems for model generators-A unifying approach
【24h】

Transition systems for model generators-A unifying approach

机译：模型生成器的过渡系统-统一方法

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

摘要

A fundamental task for prepositional logic is to compute models of prepositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for solvers developed for two other prepositional formalisms: logic programming under the answer-set semantics, and the logic PC(ID). We show that in each case the task of computing models can be seen as "satisfiability modulo answer-set programming," where the goal is to find a model of a theory that also is an answer set of a certain program. The unifying perspective we develop shows, in particular, that solvers clasp and minisat(id) are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).
机译：介词逻辑的基本任务是计算介词公式的模型。为此任务开发的程序称为可满足性求解器。我们证明了由Nieuwenhuis，Oliveras和Tinelli引入的用于建模和分析可满足性求解器的过渡系统可以适用于针对另外两种介词形式主义开发的求解器：在应答集语义下的逻辑编程和逻辑PC（ID）。我们表明，在每种情况下，计算模型的任务都可以看作是“可满足性的模答案集编程”，其目的是找到一种理论模型，该模型也是某个程序的答案集。我们开发的统一观点特别表明，尽管求解器的扣环和minisat（id）是针对不同形式主义开发的，但它们却密切相关，一个针对答案集编程，而另一个针对逻辑PC（ID）。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号