Over the past decades, Answer Set Programming (ASP) has emerged as an important paradigm for declarative problem solving. Technological progress in this area has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in non-monotonic reasoning, efforts have also been made to reconcile ASP with classical first-order logic (FO). This has resulted in the development of FO(.), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO, and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(.). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(.) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(.) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(.). Under consideration for acceptance in TPLP.
翻译:在过去几十年中,“答案设定”方案(ASP)已成为解决宣示性问题的一个重要范例;这一领域的技术进步由于使用共同标准(如ASP-Core-2语言)而得到推动;虽然ASP的根基是非口头推理,但也努力将ASP与传统的一阶逻辑(FO)相调和;这导致了FO(.)的开发,FO(.)是FO(.)的显性延伸,它使类似ASP的问题能够在纯粹的经典环境中解决;这一语言可能更容易为已经熟悉FO(.)的域专家所使用,并且可能更容易与基于经典逻辑的其他形式主义相结合;它得到了国内流离失所者推断系统的支持,该系统在一些ASP的竞争中成功地进行了竞争;然而,由于FO(.)的系统数量有限,技术进步受到阻碍;在这份文件中,我们的目标是通过将FO(.)规格转换为A-Core-2的翻译工具来弥补这一差距,从而使ASP-Core-2的解决者能够作为FO(SP)的解决方案的解决方案的解决者在当前的FO(S-S-r)中作为目前的一种解决办法的解决方案的解决方式加以展示。