模型生成器的转换系统-一种统一的方法
Transition Systems for Model Generators - A Unifying Approach
摘要：
命题逻辑的一个基本任务是计算命题公式的模型。为此任务开发的程序称为可满足性求解器。我们表明，过渡系统引入Nieuwenhuis，Oliveras和Tinelli模型和分析可满足性求解器可以适应求解器开发的其他两个命题形式主义：逻辑编程下的答案集语义，和逻辑PC（ID）。我们表明，在每种情况下，计算模型的任务可以被看作是“可满足性模答案集编程”，其目标是找到一个模型的理论，也是一个答案集的某个程序。我们开发的统一的角度来看，特别是，求解器CLASP和MINISATID是密切相关的，尽管正在开发不同的形式主义，一个答案集编程和后者的逻辑PC（ID）。
英文摘要：
A fundamental task for propositional logic is to compute models of propositional 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 propositional 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 MINISATID are closely related despite being developed for different formalisms, one for answer-set programming and the latter for the logic PC(ID).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
