Founded Semantics and Constraint Semantics of Logic Rules
Stony Brook University（石溪大学）
逻辑规则和推理是计算机科学的基础，并已得到广泛的研究。然而，逻辑语言的先验语义可能有微妙的含义，甚至在非常简单的程序上也可能存在显著的不一致，包括试图解决着名的罗素悖论。当在递归中使用无限制否定时，这些语义通常是非直观的，难以理解。本文描述了一个简单的新的语义逻辑规则，成立的语义，其直接扩展到另一个简单的新的语义，约束语义，统一的核心不同的先验语义。新的语义支持无限制否定，以及无限制存在和全称量化。它们通过允许关于谓词、规则和推理的假设被明确地指定为简单而精确的二元选择而具有独特的表达性和直观性。它们是完全声明性的，并且与先前的语义干净地相关。此外，所建立的语义可以在地面程序的大小中在线性时间内计算。
2020-03-26 cs.AI cs.DB cs.LO
Founded World Views with Autoepistemic Equilibrium Logic
udc（拉科鲁尼亚大学）；irit（图卢兹研究所）
Gelfond在1991年（G91）定义了认知规范（或程序），它是在引入主观文字的稳定模型语义下逻辑程序设计的扩展。主观文字允许检查某些常规文字在程序的所有（或部分）稳定模型中是否为真，这些模型收集在一个名为世界视图的集合中。一个认知程序可能会产生几种世界观，但在最初的G91语义学下，其中一些来自自我支持的推导。在过去的八年里，已经提出了几种替代方法来摆脱这些自我支持的世界观。不幸的是，他们的成功只能通过研究文献中的一组常见例子来衡量，因为没有正式的“自我克制”属性被定义。为了填补这一空白，我们在本文中扩展的概念，从标准的逻辑编程的认知情况下的无基集。我们定义了当一个世界观是建立在一些程序，并提出了任何语义的世界观总是成立的foundedness属性。使用反例，我们解释说，以前的方法违反成立性，并着手提出一个新的语义的基础上结合摩尔的自认知逻辑和皮尔斯的平衡逻辑。主要结果证明，这种新的语义准确地捕捉到了一套成立的G91世界观。
2019-02-20 cs.AI cs.LO
Founded (Auto)Epistemic Equilibrium Logic Satisfies Epistemic Splitting
IRIT University of Toulouse（图卢兹大学IRIT研究所）；CNRS（法国国家科学研究中心）；Universität Potsdam（波茨坦大学）
在最近的研究中，两个熟悉的概念，从逻辑编程语义（无基集和分裂）的情况下，认知逻辑程序外推。知识分裂的属性提供了一种自然和模块化的方式来理解程序没有知识周期，但令人惊讶的是，只有满足Gelfond的原始语义（G91），在文献中的许多建议。另一方面，G91可能会遭受一种自我支持的，毫无根据的推导时，认知循环发挥作用。最近，这些推导的缺失也被形式化为认知语义学的一个属性，称为基础性。此外，还提出了第一个被证明满足成立性的语义，即所谓的成立自认知平衡逻辑（FAEEL）。在本文中，我们证明了FAEEL也满足知识分裂属性的东西，连同成立性，没有履行任何其他方法到目前为止。为了证明这一结果，我们提供了一个替代的特征FAEEL的G91与一个更简单的逻辑，我们称之为建立认知平衡逻辑（FEEL），这是某种程度上的外推稳定模型语义模态逻辑S5的组合。正在考虑接受TPLP。
2020-02-20 cs.AI cs.LO
Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report
研究带差异约束的回答集编程中现有混合求解器语义基础缺乏统一逻辑基础的问题，引入HTb多类变体构建通用框架，应用于差异约束设置，揭示不同混合系统行为语义根源，形成统一框架便于相关研究。
2026-07-24 cs.AI cs.LO
Interdefinability of defeasible logic and logic programming under the well-founded semantics
Wright State University（莱特州立大学）；The University of Georgia（佐治亚大学）
我们提供了一种将努特的可废止逻辑理论转化为逻辑程序的方法，以及相应的反方向的翻译。在一定的自然约束下，歧义传播可废止逻辑ADL下的可废止理论的结论与正常逻辑程序的良基语义的结论是一致的，这说明这两种形式主义是密切相关的。使用逻辑程序到可废止理论的相同翻译，用于歧义性阻塞可废止逻辑NDL的语义可以被视为间接地为逻辑程序提供歧义性阻塞语义。我们还提供反单调算子的ADL和NDL，每个基于Gelfond-Lifschitz（GL）运营商的逻辑程序。对于没有规则上的失败者或优先级的可废止理论，ADL的运算符对应于GL运算符，因此可以被视为根据ADL部分捕获结果。类似地，NDL的运算符根据NDL捕获结果，尽管在这种情况下对理论没有限制。这两个算子都可以用来定义可废止理论的稳定模型语义。
2011-06-10 cs.AI cs.LO
Hybrid Rules with Well-Founded Semantics
Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机科学研究所）；Linköping University（林雪平大学）
一个通用的框架，提出了集成的规则和外部一阶理论。它以一般逻辑程序的良基语义为基础，并受到约束逻辑程序设计（CLP）和逻辑程序的构造性否定思想的启发。混合规则是在主体中扩展了约束的普通子句;约束是外部理论语言中的某些公式。混合程序是一组混合规则和一个外部理论的组合.通过指定外部理论的类和约束的类来获得框架的所有权。一个例子是集成（非析取）数据库与本体形式化为描述逻辑。本文定义了混合程序的声明语义和目标驱动的形式化操作语义。后者可以看作是SLS-归结的推广。它提供了一个基础的混合实现结合Prolog与约束求解器。证明了操作语义的合理性。给出了声明语义可判定性和操作语义完备性的充分条件。
2009-06-20 cs.AI cs.LO cs.PL
Abduction in Well-Founded Semantics and Generalized Stable Models
溯因逻辑程序设计提供了一种形式化的表达和解决问题的领域，如诊断，规划，信念修正和假设推理。表逻辑程序设计提供了一种计算机制，它提供了一种优于Prolog的声明性级别，并支持在诸如解析、程序分析和模型检验等领域的成功应用。在本文中，我们将展示如何使用表格逻辑编程来评估查询溯因框架的完整性约束时，这些框架包含默认和显式否定。其结果是能够在有明确否定和答案集的良好基础的语义上计算溯因。我们的方法包括一个转换和评估方法。该转换与程序中的每个目标文字$O$相邻，目标文字$not(O)$以及确保当且仅当$O$为假时$not(O)$为真的规则。我们把得到的程序称为{ \em dual}程序。然后，评估方法\wfsmeth对对偶程序进行操作。\wfsmeth{}是健全和完整的评估查询溯因框架的蕴涵方法是基于显式否定的良好的基础语义，或回答集。此外，\wfsmeth{}是渐近有效的任何已知的方法为任一类的问题。此外，当绑架是不希望的，\wfsmeth{}操作的双重程序提供了一种新的制表方法，用于评估查询地面扩展程序的复杂性和终止属性是类似的最好的制表方法的良好的基础语义。一个公开可用的元解释器已经开发了\wfsmeth{}使用XSB系统。
2003-12-24 cs.AI cs.LO
On the problem of computing the well-founded semantics
良基语义是含否定的逻辑程序研究和应用最广泛的语义之一。在有限命题程序的情况下，它可以在多项式时间内计算，更具体地说，在O（|（P）|size（P））步，其中size（P）表示逻辑程序P中原子出现的总数。该界限由Van Gelder引入的算法实现，该算法被称为交替不动点算法。对交替不动点算法的改进是困难的。在本文中，我们研究的交替不动点方法的扩展和修改。然后，我们限制我们的注意力类的程序，其规则有不超过一个积极的发生在他们的身体的原子。对于该类程序，我们提出了一种新的交替不动点方法，其中假原子以自上而下的方式计算。我们表明，我们的算法比其他已知的算法更快，对于广泛的一类程序，它是线性的，所以，渐近最优。
2001-01-17 cs.AI cs.DS cs.LO
Axe 'Em: Eliminating Spurious States with Induction Axioms
针对一阶逻辑（FOL）抽象建模中因语义差距导致的虚假状态问题，提出利用归纳公理精炼良基/有限域语义的方法，通过OSC片段归约证明可判定性，原型工具验证了其有效性。
2024-11-29 cs.LO cs.PL
A Logic for Non-Monotone Inductive Definitions
著名的归纳法原理包括单调归纳法和各种非单调归纳法，如膨胀归纳法、良基集上的归纳法和迭代归纳法。在这项工作中，我们定义了一个逻辑形式化归纳良好的基础集和单调和迭代归纳。正如正归纳原理已在FO（LFP）中形式化，膨胀归纳原理已在FO（IFP）中形式化一样，本文在一种新的非单调归纳定义逻辑（ID-逻辑）中形式化了迭代归纳原理。逻辑的语义受到逻辑编程的良基语义的强烈影响。我们的主要结果是关于ID逻辑中归纳定义的模性质。具体而言，我们制定的条件下，同时定义$\D$的几个关系是逻辑上等同于一个连接的较小的定义$\D_1 \land ... \land \D_n$与不相交的定义谓词。这个结果的困难来自这样一个事实，即分别在$\D_i$和$\D_j$中定义的谓词$P_i$和$P_j$可以通过同时归纳相互连接。由于良基语义下的逻辑程序设计和溯因逻辑程序设计是我们的逻辑的适当片段，我们的模块性结果也适用于那里。
2005-01-13 cs.AI cs.LO
Enhancing Global SLS-Resolution with Loop Cutting and Tabling Mechanisms
全局SLS解析是一种众所周知的过程语义，用于在有根据的模型下自上而下计算查询。它继承了SLDNF-解析的{ \em linearity}属性，这使得使用简单的基于堆栈的存储器结构可以轻松有效地实现。然而，像SLDNF-分辨率，它遭受的无限循环和冗余计算的问题。为了解决这个问题，在本文中，我们开发了一个新的过程语义，称为{ \em SLTNF-resolution}，通过增强全局SLS-分辨率与循环切割和制表机制。SLTNF-分辨率是健全和完整的w.r.t.该方法为具有有界项大小性质的逻辑程序提供了良基语义，优于已有的线性制表过程语义，如SLT-解析.
2005-07-14 cs.AI cs.LO
An Environment for the Exploration of Non Monotonic Logic Programs
稳定模型语义和良好基础语义已经被证明是非常有用的几个应用程序的非单调推理。然而，稳定模型呈现高计算复杂性，而良好基础语义易于计算并且提供稳定模型的近似。对于逻辑程序的两种语义都存在有效的引擎。这项工作提出了两个这样的系统，即XSB和SMODELS的计算集成。由此产生的系统被称为XNMR，并提供了一个交互式的系统，用于探索这两种语义。模块化等方面可以利用，以方便调试大型知识库与通常的Prolog调试技术和交互式环境。此外，使用完整的Prolog系统作为Stable Models引擎的前端，增强了此类系统通常接受的语言。
2001-11-19 cs.LO cs.PL
An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
基于Lifschitz的最小知识否定失败逻辑的混合知识库是将描述逻辑和逻辑程序设计的表达能力结合在一种语言中的成功方法。它们的语法由Motik和Rosati定义，不允许函数符号。为了给MKNF HKB定义一个有根据的语义，Knorr等人定义了一个出现在其中的模态原子的划分，称为交替不动点划分。在本文中，我们提出了一个迭代不动点语义的HKB函数符号。我们证明，我们的语义扩展Knorr等。的，因为对于无函数的HKB，它与其交替不动点划分一致。所提出的语义适合于概率扩展与分布语义的方法，这是未来工作的主题。
2022-08-05 cs.LO
Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics (Extended Version)
本文将经典稳定模型和良基语义重构于近似不动点理论框架内，扩展其至多值逻辑，并应用于模糊逻辑程序设计，澄清语义关系、推广分层概念并设计更精确变体。
2025-07-16 cs.LO
On the Equivalence Between Abstract Dialectical Frameworks and Logic Programs
Autonomous University of Juarez（华雷斯自治大学）
抽象辩证框架（Abstract Dialectical Frameworks，ADF）是一种论证框架，其中每个节点都与一个接受条件相关联。这使我们能够将不同类型的依赖关系建模为支持和攻击。以往的研究提供了一个从正常逻辑程序（NLP）到ADF的翻译，并证明了正常逻辑程序的稳定模型语义与相应的ADF的语义是等价的。然而，这些研究未能确定一个语义的ADF相当于一个三值语义（部分稳定的模型和良好的基础模型）的NLP。在这项工作中，我们专注于ADF的一个片段，称为攻击辩证框架（ADF $^+$ s），并提供了一个翻译从NLP ADF $^+$ s鲁棒足以保证部分稳定模型之间的等价性，良好的基础模型，定期模型，稳定的模型语义NLP和相应的完整模型，接地模型，首选模型，稳定的模型ADF。此外，我们定义了一个新的语义ADF $^+$ s，称为L-稳定，并显示它是等价的L-稳定的语义NLP。本文件正在考虑被TPLP接受。
2019-07-22 cs.AI cs.LO
Towards a Systematic Account of Different Semantics for Logic Programs
在[Hitzler and Wendt 2002，2005]中，已经提出了一种新的方法，该方法允许导出具有否定的逻辑程序的不同声明性语义的统一表征。这项工作的一个结果是，良好的基础语义可以正式理解为Fitting（或Kripke-Kleene）语义的分层版本。然而，导致这一结果的结构显示出某种不对称性，这是不容易理解的。我们将在这里研究这种情况，其结果是，我们将获得正常逻辑程序的不同语义之间的关系的连贯画面。
2005-02-22 cs.AI cs.LO
A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems
Yale University（耶鲁大学）；SingularityNET（奇点网）
我们引入了一个正式的元语言的概率编程，能够表达程序和类型系统中，他们被嵌入。我们的动机是希望AGI不仅学习相关知识（程序/证明），而且学习适当的推理方式（逻辑/类型系统）。我们利用立方类型论和依赖类型元图的框架来形式化我们的方法。在这样做时，我们表明，元语言中的特定结构可以通过互模拟（意味着路径等价）与它们对应的类型系统相关。这使得我们的方法提供了一种方便的方法来派生合成指称语义的各种类型系统。特别是，我们推导出纯型系统（PTS）和概率依赖型系统（PDTS）的互模拟。我们进一步讨论了PTS的关系，非良基集理论，并证明了我们的方法的可行性与实现的互模拟证明在一个守护立方类型论类型检查。
2022-08-16 cs.AI cs.FL cs.LO
The Intricacies of 3-Valued Extensional Semantics for Higher-Order Logic Programs
In（Bezem 1999; Bezem 2001），M. Bezem为正高阶逻辑程序定义了一种扩展语义。最近，在Rondogiannis和Symeonidou 2016中证明了Bezem的技术可以扩展到具有否定的高阶逻辑程序，保留其扩展属性，前提是它在具有无限数量真值的逻辑下解释。在（Rondogiannis和Symeonidou 2017）中，还证明了Bezem的技术，当在稳定模型语义下扩展时，通常不会导致扩展稳定模型。在本文中，我们考虑的问题，扩展Bezem的技术下的良基语义。我们证明了在一般情况下，良好的理由扩展未能保留外延。在积极的一面，我们证明，分层高阶逻辑程序，可拓性确实实现。我们分析了在一般情况下外延性失败的原因，认为三值设置不能区分某些谓词，这些谓词似乎在程序上下文中具有不同的行为，但恰好与三值关系相同。该文件正在考虑被TPLP接受。
2017-07-15 cs.LO cs.PL
Graph-based Interpretation of Normal Logic Programs
在本文中，我们提出了一个依赖图为基础的方法来计算正常的逻辑程序的各种语义。我们的方法采用\textit{conjunction nodes}明确表示正常的逻辑程序的依赖图。该依赖图可以以语义保持的方式进行适当的转换，并重新转换为等价的正常逻辑程序。这种转换后的正规逻辑程序可以用回答集编程（ASP）中编写的一些规则来扩充，并使用CLINGO系统来计算其回答集。根据这些附加规则在ASP中的编码方式，可以在稳定模型语义、良基语义或共稳定模型语义下计算原始正常逻辑程序的模型。在每种情况下，也会生成模型中每个原子的对齐。我们报告我们的方法的实施以及其性能评估。
2021-11-25 cs.LO
The Power of Negation in Higher-Order Datalog
Harokopio University of Athens（哈罗基皮奥雅典大学）；University of Ioannina（约阿尼纳大学）；National and Kapodistrian University of Athens（国家与卡波迪斯特里阿斯雅典大学）
本文研究了高阶Datalog$^\neg$在不同语义下的表达能力，证明其在well-founded语义下捕捉k-EXP，并在stable模型语义下捕捉co-(k-NEXP)和k-NEXP，揭示了顺序与非确定性之间的权衡。
2025-07-27 cs.CC cs.DB cs.LO
The Stable Model Semantics for Higher-Order Logic Programming
Vrije Universiteit Brussel（布鲁塞尔自由大学）；Katholieke Universiteit Leuven（鲁汶大学）；Harokopio University of Athens（雅典哈罗科皮奥大学）；National and Kapodistrian University of Athens（雅典国立与卡波迪斯特里亚大学）
本文基于近似不动点理论，为高阶逻辑程序提出稳定模型语义，推广经典二值与三值语义，并定义分层程序类，证明其唯一稳定模型与良基语义一致，为新型ASP系统奠定基础。
2024-08-20 cs.AI cs.LO cs.PL
Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics
本文通过证明论技术提出直觉主义 Gödel-Löb 逻辑 IGL，包含盒与菱形模态，并证明其带标签系统与双关系语义中逆良基复合条件等价，主要贡献在于完备性证明需经多个中间刻画。
2023-09-01 cs.LO math.LO
Hybrid MKNF with Classical Negation in the Rule Component
Université Clermont Auvergne, LIMOS, CNRS France（克莱蒙特大学，LIMOS，CNRS法国）
研究混合MKNF知识库在规则组件中不支持经典否定的问题，提出扩展混合MKNF以支持经典否定，定义其语法和语义并给出计算有充分根据模型的过程，增强了表示显式否定知识的能力。
2026-07-24 cs.AI cs.LO cs.SC
XNMR: A tool for knowledge bases exploration
XNMR是一个系统，旨在探索的结果相结合的良基语义系统XSB与稳定模型评估SMODELS。它的主要目标是作为一种工具，用于快速和交互式地探索知识库。
2000-03-13 cs.AI cs.LO
Corollaries on the fixpoint completion: studying the stable semantics by means of the Clark completion
一般逻辑程序P的不动点完备化fix（P）是一种程序变换，使得P的稳定模型恰好是fix（P）的Clark完备化模型。这是众所周知的，并由Dung和Kanchanasut（1989）进行了研究。然而，这种对应关系更进一步：P的Gelfond-Lifschitz算子与fix（P）的直接结果算子一致，如Wendt（2002）所示，甚至延续到用于表征良基语义和Kripke-Kleene语义的标准算子。我们将应用这些知识的稳定语义的研究，这将使我们几乎毫不费力地得出新的结果，有关固定点和基于度量的语义，神经符号积分。
2004-02-09 cs.AI cs.LO
Knowledge Compilation of Logic Programs Using Approximation Fixpoint Theory
出现在逻辑程序设计的理论与实践（TPLP），ICLP 2015会议录知识编译的最新进展介绍了将\emph{positive}逻辑程序编译为命题逻辑的技术，主要是利用最小不动点计算的构造性。这种方法与现有方法相比有几个优点：它保持逻辑等价性，不需要（昂贵的）循环中断预处理或引入辅助变量，并且显著优于现有算法。不幸的是，这种技术仅限于\emph{negation-free}程序。在本文中，我们展示了如何将它扩展到一般的逻辑程序下的良基语义。我们在近似不动点理论中开展工作，这是一个代数框架，它统一了不同逻辑的语义。因此，我们的代数结果也适用于自认识逻辑，缺省逻辑和抽象辩证框架。
2015-07-23 cs.LO
A uniform approach to logic programming semantics
逻辑编程和非单调推理的部分理论涉及这些范式的不动点语义研究。在过去的二十年里，已经提出了几种不同的语义，其中一些比其他的更成功和更受认可。这些不同的语义背后的原理是多种多样的，这取决于一个人的观点，这可能是一个程序员的观点，也可能是受常识推理的启发，因此导致这些语义的结构在技术上是非常多样的，它们之间的确切关系还没有被完全理解。在本文中，我们提出了一个概念上的新方法，基于层次映射，它允许提供统一的表征不同的语义逻辑程序。我们将展示我们的方法，给出新的和统一的一些主要的语义，更特别的最小模型的语义明确的程序，拟合语义，和良好的基础语义的表征。弱完美模型语义的一个新的表征也将提供。
2003-11-12 cs.AI cs.LO
Fixpoint 3-valued semantics for autoepistemic logic
本文提出了一种自认知逻辑（AEL）的构造性不动点语义。这个不动点刻画了一个自认知理论的唯一但可能是三值的信念集。它可以是三值的，因为对于公式F的子类，不动点可能不指定F是否被相信。本文提出了一种自认知逻辑（AEL）的构造性三值语义。我们引入了一个派生操作符，并定义其最小不动点的语义。语义是3值的，在这个意义上，对于某些公式，最小不动点并不指定它们是否被相信。我们证明了导子算子的完全不动点对应于Moore稳定展开式。在逻辑程序的模态表示的情况下，我们的最小不动点语义表示良基语义或3值Fitting-Kunen语义（取决于所使用的嵌入）。我们表明，在计算上，我们的语义是简单的摩尔提出的语义（假设多项式层次结构不崩溃）。
1999-01-12 cs.AI cs.LO
Diamonds Are Forever: Stabilization Semantics for Unrestricted Aggregation and Recursion in Logica
Google LLC（谷歌有限责任公司）；University of Illinois, Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Gonzaga University（贡萨加大学）
针对 Logica 语言中自由组合递归与聚合带来的语义挑战，提出 Defendant-Opponent (DO) 语义，一种基于稳定化的非单调逻辑程序语义框架，并通过博弈论和模态逻辑两种等价刻画，兼容传统不动点语义并为无不动点收敛程序提供严格解释。
2026-06-03 cs.LO
Knowledge of Uncertain Worlds: Programming with Logical Constraints
Stony Brook University（石溪大学）
复杂应用程序的逻辑编程必须处理递归和否定，这两者一起在逻辑中产生了重大挑战，导致许多不同的，相互冲突的规则语义。本文描述了一种统一的语言，DA逻辑，设计和分析逻辑，统一的基础语义和约束语义的基础上，支持的权力和不同的意图语义编程的易用性。其关键思想是提供元约束，支持使用不确定信息的形式，无论是未定义的值或可能的组合值或两者兼而有之，并促进使用的知识单元，可以实例化的任何新的谓词，包括谓词与额外的参数。
2020-12-11 cs.AI cs.LO cs.PL
Computing and Comparing Semantics of Programs in Multi-valued Logics
可以分配给逻辑程序的不同语义对应于关于原子的不同假设，这些原子的逻辑值不能从规则中推断出来。因此，有根据的语义对应于每个这样的原子都是假的假设，而Kripke-Kleene语义对应于每个这样的原子都是未知的假设。在本文中，我们提出了统一和扩展这种基于解析的方法，通过引入参数化语义的逻辑程序。该参数保存的值是为所有原子假定的值，这些原子的逻辑值不能从规则中推断出来。我们工作在具有双格结构的多值逻辑中，并考虑Fitting定义的一类逻辑程序。按照Fitting的方法，我们定义了一个简单的运算符，它允许我们计算参数化的语义，并比较和组合针对不同参数值获得的语义。Fitting提出的语义对应于值false。我们还表明，我们的方法捕获和扩展常规逻辑程序的通常语义，从而统一其计算。
2000-02-18 cs.DB cs.LO
Enablers and Inhibitors in Causal Justifications of Logic Programs
University of Corunna（拉科鲁尼亚大学）
出现在逻辑编程理论与实践（TPLP）中。在本文中，我们提出了一个扩展的逻辑编程（LP），其中每个默认文字来自良好的基础模型相关联的理由表示为一个代数表达式。这个表达式包含因果解释（以规则标签构建的证明图的形式）和否定范围内的术语，这些术语代表启用或禁用因果规则应用的条件。使用一些例子，我们讨论了这些新的条件，我们分别称之为“使能”和“抑制剂”，是密切相关的默认否定，并有一个本质上不同的性质，从定期的因果关系。最重要的结果是一个正式的比较，最近的代数方法的理由在LP：“为什么不种源”（WESTERN）和“因果图”（CG）。我们表明，目前的方法扩展了WESTERN和CG的理由下的基础良好的语义，作为副产品，我们还建立了这两种方法之间的正式关系。
2016-02-22 cs.AI cs.LO
A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification
本文讨论的问题，指定，模拟和验证反应系统重写逻辑。它提出了一个可执行的语义概率，时间和空间并发约束编程-这里称为随机和空间并发约束系统（SSCC）-在重写逻辑语义框架。该方法是基于一个增强和广义模型的并发约束规划（CCP）的计算层次空间可以分配给属于代理。可执行语义忠实地表示和操作捕捉高度并发的性质，不确定的行为，空间和认知特征的反应系统与信息流。在SSCC中，定时属性（由随机持续时间表示）可以与进程相关联，并且还支持排他性和独立的概率选择。利用Maude系统中的SMT求解技术，实现了SSCC的底层约束系统，包括整数和实数上的无量词公式。这导致了一个完全可执行的实时符号规范，可用于定量分析的统计模型检验的形式。SSCC的主要特点和能力说明了整个文件的例子。这一贡献是一个更大的研究工作的一部分，旨在提供正式的分析技术和工具，数学上建立在CCP的方法，研究界。
2022-11-03 cs.LO
On systematic construction of correct logic programs
本文提出一种声明式方法，在Kunen三值完成语义和良基语义下，针对给定规范系统化构造可证明正确且半完备的正规逻辑程序，方法简单且适用于日常编程。
2025-08-22 cs.LO cs.SE
Contextual hypotheses and semantics of logic programs
The University of New South Wales（新南威尔士大学）
逻辑程序设计已经发展成为一个丰富的领域，建立在一个逻辑基础之上，其主要组成部分是一种非经典形式的否定，有时与经典否定共存。该领域已经出现了许多替代语义，其中Kripke-Kleene语义，良好基础语义，稳定模型语义和答案集语义是最成功的。我们表明，所有上述语义的通用语义的特殊情况下，在一个框架中，经典否定是否定的独特形式，在那里的字面量的机构的规则可以“标记”，以表明它们可以是目标的假设。一个特定的语义就等于选择一个特定的标记方案和选择一组特定的假设。当文字属于所选择的假设集合时，该文字在规则的主体中的所有标记的出现都被假定为真，而该文字在规则的主体中未被标记的出现将被导出以便有助于规则的触发。因此，在这个框架中提出的假设推理的概念不是基于做出全局假设，而是更巧妙地基于做出局部的、上下文的假设，根据所选择的一组假设，按照所选择的标记方案所指示的那样发挥作用。我们的方法提供了一个统一的观点，在逻辑编程中提出的各种语义，经典的，只有经典的否定被使用，并链接的语义逻辑程序的机制，赋予基于规则的系统的权力，利用假设推理。
2011-05-06 cs.AI cs.LO
Minimum Model Semantics for Logic Programs with Negation-as-Failure
我们给出了一个纯粹的模型理论表征的语义逻辑程序与否定作为失败允许在条款机构。在我们的语义程序的意义是，在经典的情况下，唯一的最小模型在一个程序独立的顺序。我们使用一个扩展的真值域，它在False（最小值）和True（最大值）之间有一个不可数的线性有序真值集，中间有一个零元素。低于零的真值像可数序数一样排序。大于零的值的顺序正好相反。否定被解释为关于零的反射，然后是向零的一步;唯一不受否定影响的真值是零。我们证明了每个程序都有唯一的极小模型M_P，并且这个模型可以用T_P迭代来构造，T_P迭代是通过可数序数进行的。此外，我们还证明了M_P也可以通过一个模型交构造来获得，该构造推广了经典逻辑程序设计中著名的模型交定理。最后，我们证明了通过将无穷值模型M_P的真值和假值折叠为（经典的）真值和假值，我们得到了一个与良基模型相同的三值模型。
2003-06-03 cs.AI cs.LO cs.PL
On the Trap Space Semantics of Normal Logic Programs
Inria Saclay, EP Lifeware, Palaiseau, France（法国萨克莱研究所、EP Lifeware、Palaiseau）；LIRICA team, LIS, Aix-Marseille University, Marseille, France（LIRICA团队、LIS、艾克斯-马赛大学、马赛）
本文提出陷阱空间语义作为正常逻辑程序的新解释方法，结合模型论和动态特性，统一证明支持类、严格稳定类和常规模型的存在性，并揭示现有语义间的深层关系。
2026-01-07 cs.AI cs.LO
Stable models and an alternative logic programming paradigm
在本文中，我们重新审视的地方和作用的稳定模型语义在逻辑编程和对比，它与最少Herbrand模型的方法霍恩程序。我们证明了稳定模型语义的固有特征自然会导致一个逻辑编程系统，提供了一个有趣的替代更传统的逻辑编程风格的霍恩逻辑编程，分层逻辑编程和逻辑编程与良好的基础语义。所提出的方法是基于程序条款的约束的解释。在这种情况下，程序不描述一个单一的预期模型，而是一系列稳定的模型。这些稳定的模型编码解决方案的约束满足的问题所描述的程序。我们的方法对逻辑程序的语法施加了限制。特别是，函数符号被从语言中删除。我们认为，由此产生的逻辑编程系统是很好地协调NP类的问题，有一个定义明确的应用领域，和一个新兴的编程方法。我们指出，是什么使整个方法可行的算法来计算命题逻辑程序的稳定模型的实现的最新进展。
1998-09-18 cs.AI cs.LO
Extending Coinductive Logic Programming with Co-Facts
我们引入了一个广义的逻辑编程范式，程序，由事实和规则与通常的语法，可以丰富的共同事实，语法上类似的事实，但有一个特殊的意义。在共归纳逻辑程序设计中，解释是完全Herbrand基的子集，包括无限项。然而，程序的意图（声明性语义）是一个固定点，它不一定是最小的，也不一定是最大的，而是由共同事实决定的。通过这种方式，可以在非良基结构上表达谓词，例如无限列表和图，对于这些结构，共归纳解释不够精确。此外，这种范式很好地包含了标准（归纳）和共归纳逻辑编程，因为两者都可以通过特定的共事实选择来表达，因此归纳谓词和共归纳谓词可以共存于同一个程序中。通过实例对该范式进行了说明，并给出了声明语义和操作语义，证明了操作语义的正确性。最后，我们描述了一个原型元解释器。
2017-09-14 cs.LO cs.PL
Games and Argumentation: Time for a Family Reunion!
本文指出论证框架中的击败规则与博弈中的获胜规则高度相似，回顾了数据库理论中win-move查询的关键成果，并引入博弈概念为论证框架提供新视角，利用查询评估博弈解释结果的溯源。
2023-09-12 cs.LO
CP-logic: A Language of Causal Probabilistic Events and Its Relation to Logic Programming
Katholieke Universiteit Leuven（天主教鲁汶大学）
本文发展了一种表示概率因果律的逻辑语言。我们对这种语言的兴趣是双重的。首先，它可以作为因果知识表示的基础研究。因果关系具有内在的动态方面，Shafer在他的概率树框架中已经在语义层面上进行了研究。在这样一个动态的背景下，考虑到一个领域随时间的演变，因果律作为指导这种演变的东西的想法是很自然的。在我们的形式化，一组概率因果律可以用来表示一类概率树在一个简洁，灵活和模块化的方式。通过这种方式，我们的工作扩展了Shafer的语义对象提供了一个方便的逻辑表示。其次，这种语言也与概率逻辑编程领域相关。特别是，我们证明，在我们的语言的理论的形式语义可以等价地定义为概率分布在良好的基础模型的某些逻辑程序，使它正式非常类似于现有的语言，如ICL或PRISM。因为我们可以用一种完全独立的方式来激发和解释我们的语言，将其作为概率因果律的表示，这就为解释这种概率逻辑程序背后的直觉提供了一种新的方式：我们可以用非逻辑学家同样可以理解的术语来精确地说这种程序表达了哪些知识。此外，我们还获得了一个额外的一块知识表示方法的概率逻辑程序，通过展示他们如何表达概率因果律。
2009-04-10 cs.AI cs.LO
