Founded semantics and constraint semantics of logic rules

Founded semantics and constraint semantics of logic rules
复制标题

DOI：
10.1093/logcom/exaa056
复制
发表时间：
2020-10
期刊：
J. Log. Comput.
影响因子：
--
通讯作者：
Yanhong A. Liu;S. Stoller
Yanhong A. Liu;S. Stoller
中科院分区：
其他
文献类型：
--
作者：
Yanhong A. Liu;S. Stoller

文献摘要

相似文献

逻辑规则和推理是计算机科学的基础，已经被广泛研究。然而，逻辑语言的先验语义可能有微妙的含义，甚至在非常简单的程序上也可能存在显著的不一致，包括试图解决着名的罗素悖论。当在递归中使用无限制否定时，这些语义通常是非直观的，难以理解。本文描述了一个简单的新的语义逻辑规则，成立的语义，其直接扩展到另一个简单的新的语义，约束语义，统一的核心不同的先验语义。新的语义支持无限制否定，以及无限制存在和全称量化。它们是唯一的表达和直观的，允许关于谓词，规则和推理的假设被明确指定，作为简单而精确的二元选择。它们是完全声明性的，并且与先前的语义干净地相关。此外，所建立的语义可以在地面程序的大小中在线性时间内计算。
Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell’s paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in recursion. This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates, rules and reasoning to be specified explicitly, as simple and precise binary choices. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program.