Proceedings 38th International Conference on Logic Programming
ICLP是展示逻辑编程研究的首要国际活动。对ICLP 2022的贡献是在逻辑编程的所有领域，包括但不限于：基础：语义学，形式主义，非单调推理，知识表示。语文问题：并发，对象，协调，移动性，高阶，类型，模式，断言，模块，元编程，基于逻辑的特定领域语言，编程技术。编程支持：程序分析、转换、验证、验证、分析、测试、执行可视化。实施情况：编译、虚拟机、存储管理、并行和分布式执行、约束处理规则、制表、外部接口、用户界面。相关范例和协同作用：归纳和共归纳逻辑编程，约束逻辑编程，答案集编程，与SAT，SMT和CSP求解器的交互，定理证明，论证，概率编程，机器学习。应用领域：数据库、大数据、数据集成和联邦、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、网络安全、机器人技术、教育。
2022-08-04 cs.AI cs.LO
Transaction Logic with (Complex) Events
CENTRIA - Dep. de Informática（人工智能与计算机科学研究中心）
这项工作涉及的问题相结合的反应功能，如响应事件和定义复杂事件的能力，在一般的知识库（KBs）的事务的执行。以此为目标，我们建立在事务逻辑（TR）上，这是一种精确设计的逻辑，用于在任意逻辑理论定义的KB中建模和执行事务。在它中，事务以逻辑编程风格编写，通过将通用KB上的原始更新操作与通常的逻辑编程连接词和一些额外的连接词相结合，例如用于表达动作序列。虽然TR是处理事务的自然选择，但TR是否可以用于表示复杂事件，以及同时处理复杂事件的检测和事务的执行仍然是一个问题。在本文中，我们表明，前者是可能的，而后者是不。为此，我们首先说明TR如何表达复杂事件，特别是如何在逻辑中翻译SNOOP事件表达式。之后，我们展示了为什么TR不能同时处理这两个问题，并提出了带事件的事务逻辑，它的语法，模型理论和执行语义来解决预期的问题。所实现的解决方案是TR的非单调扩展，它保证了在事务中检测到的每个复杂事件都必须得到响应。
2014-05-15 cs.AI cs.LO
Proceedings 40th International Conference on Logic Programming
University of Texas at Dallas（德克萨斯大学达拉斯分校）
该论文集收录第40届国际逻辑程序设计会议（ICLP）的技术内容，涵盖逻辑程序设计的语义、语言设计、程序分析及实现方法学等领域，展现该领域的最新研究成果。
2025-02-11 cs.AI cs.LO
Proceedings 37th International Conference on Logic Programming (Technical Communications)
ICLP是展示逻辑编程研究的首要国际活动。对ICLP 2021的贡献是在逻辑编程的所有领域，包括但不限于：基础：语义学，形式主义，非单调推理，知识表示。语文问题：并发，对象，协调，移动性，高阶，类型，模式，断言，模块，元编程，基于逻辑的特定领域语言，编程技术。编程支持：程序分析、转换、验证、验证、分析、测试、执行可视化。实施情况：编译、虚拟机、存储管理、并行和分布式执行、约束处理规则、制表、外部接口、用户界面。相关范例和协同作用：归纳和共归纳逻辑编程，约束逻辑编程，答案集编程，与SAT，SMT和CSP求解器的交互，定理证明，论证，概率编程，机器学习。应用领域：数据库、大数据、数据集成和联邦、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、网络安全、机器人技术、教育。
2021-09-15 cs.AI cs.LO
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
SLT-Resolution for the Well-Founded Semantics
全局SLS-归结和SLG-归结是自顶向下评价一般逻辑程序良基语义的两种典型机制。全局SLS解析对于查询评估是线性的，但是遭受无限循环和冗余计算。相比之下，SLG-归结通过制表来解决无限循环和冗余计算，但它不是线性的。非线性方法的主要缺点是，它不能使用简单，有效的基于堆栈的内存结构来实现，也不能很容易地扩展到处理一些严格的顺序运算符，如Prolog中的cuts。在本文中，我们提出了一个线性制表方法，称为SLT-分辨率，自顶向下的评价良好的基础语义。SLT-分辨率是SLDNF-分辨率与制表的实质性扩展。它的主要特点包括：（1）在保持线性的同时，解决了无限循环和冗余计算问题。(2)它是终止的，声音和完整的w.r.t.有界项大小属性与非挣扎查询的程序的良基语义。它的时间复杂度与无函数逻辑程序的SLG-归结和多项式相当。(3)由于它的线性查询评估，SLT-分辨率的桥梁之间的差距，良好的基础语义和标准的Prolog实现技术。它可以通过扩展到任何现有的Prolog抽象机器（如WAM或ATOAM）来实现。
2001-03-02 cs.AI cs.PL
Termination Proofs for Logic Programs with Tabling
表格逻辑编程在逻辑编程社区中越来越受到关注。它避免了SLD执行的许多缺点，并为逻辑程序提供了一种更灵活且通常非常有效的执行机制。特别地，逻辑程序的表格执行比基于SLD解析的执行更频繁地终止。在这篇文章中，我们介绍了两个概念的通用终止逻辑编程与Tabling：准终止和（更强的概念）LG终止。我们提出了这两个概念的终止，即准可接受性和LG-可接受性的充分条件，我们表明，这些条件也是必要的情况下，制表是精心挑选的。从这些条件出发，我们给出了模终止证明，即，证明能够组合单独程序的终止证明以获得组合程序的终止证明。最后，在模式信息的存在下，我们陈述了充分条件，这些条件构成了以基于约束的方式自动证明终止的基础。
2000-03-09 cs.LO
Proceedings 35th International Conference on Logic Programming (Technical Communications)
自1982年在马赛举行第一次会议以来，ICLP一直是展示逻辑编程研究的首要国际活动。在逻辑编程的所有领域寻求贡献，包括但不限于：基础：语义学，形式主义，非单调推理，知识表示。语言：并发，对象，协调，移动性，高阶，类型，模式，断言，模块，元编程，基于逻辑的领域特定语言，编程技术。声明式编程：声明式程序开发，分析，类型和模式推理，部分求值，抽象解释，转换，验证，验证，编译，分析，测试，执行可视化实现：虚拟机，编译，存储管理，并行/分布式执行，约束处理规则，制表，外部接口，用户界面。相关范例和协同作用：归纳和协同归纳逻辑程序设计、约束逻辑程序设计、答案集程序设计、与SAT、SMT和CSP求解器的交互、类型推断和定理证明的逻辑程序设计技术、论证、概率逻辑程序设计、与面向对象和函数式程序设计的关系。应用领域：数据库、大数据、数据集成和联合、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、教育、网络安全和机器人技术。
2019-09-17 cs.AI cs.LO cs.PL
Planning as Tabled Logic Programming
CUNY Brooklyn College and Graduate Center（纽约市立大学布鲁克林学院及研究生中心）；Charles University（查理大学）；Univ. di Udine（乌迪内大学）
本文介绍了Picat的规划器及其实现，以及2014年国际规划竞赛（IPC）中使用的几个领域的规划模型。Picat的规划器是用制表法实现的。在搜索过程中，遇到的每个状态都被表化，表化的状态用于有效地执行资源受限搜索。在Picat中，结构化数据可以用来避免枚举所有可能的对象排列，术语共享用来避免公共状态数据的重复。本文提出了几种建模技术，通过示例模型，从设计状态表示，以促进数据共享和对称性破缺，编码操作的操作，有效的前提条件检查和状态更新，结合领域知识和算法。广泛地说，本文证明了有效的表格逻辑规划，并认为建模的重要性，尽管最近取得了重大进展，独立于域的PDDL规划。
2015-07-14 cs.AI
ECA-RuleML: An Approach combining ECA Rules with temporal interval-based KR Event/Action Logics and Transactional Update Logics
事件驱动架构（EDA）中需要解决的一个重要问题是如何正确有效地捕获和处理基于事件/动作的逻辑。本文致力于弥合之间的差距的知识表示（KR）方法的基础上持久的事件/动作和事件演算等形式主义，一方面，和事件-条件-动作（ECA）反应规则扩展的主动数据库的方法，查看事件的瞬时发生和/或事件序列，另一方面。我们提出了基于反应规则（ECA规则）和一种新的基于间隔的事件逻辑的形式主义，并提出了具体的基于规则ML的语法，语义和实现。我们进一步评估这种方法的理论，实验和一个例子来自常见的行业用例，并说明其好处。
2006-11-10 cs.AI cs.LO cs.MA
Evidential Transactions with Cyberlogic
fortiss（福蒂斯研究所）；SRI International（SRI国际）
本文提出 Cyberlogic 这一用于构建和分析数字证据交易的逻辑基础，通过扩展直觉主义谓词逻辑引入证明与知识模态，将公钥映射为授权、交易定义为分布式逻辑程序并利用分布式证明搜索收集可验证证据，支持信任、委托与撤销等策略，并提出了策略保密下的函数加密证书检查方案。
2023-03-20 cs.AI cs.CR cs.LO
On Combining Linear-Based Strategies for Tabled Evaluation of Logic Programs
表求值是一种公认的、功能强大的技术，它克服了传统Prolog系统在处理递归和冗余子计算方面的局限性。我们可以区分两个主要类别的制表机制：基于悬浮的制表和线性制表。虽然基于挂起的机制通常被认为获得更好的结果，但它们具有更多的存储空间需求，并且比线性制表机制更复杂和更难实现。可以说，SLDT和RSDT策略是标准线性表格评估的两个最成功的扩展。在这项工作中，我们提出了一个新的战略，命名为DRS，我们提出了一个框架，顶部的雅普系统，支持所有这三个战略的组合。我们的实现共享底层执行环境和用于在Yap中实现制表的大多数数据结构。因此，我们认为，所有这些共同的特点，使我们能够在这些不同的线性制表策略之间进行第一次和公平的比较，因此，更好地了解各自的优点和缺点，当单独使用或与其他组合。
2011-07-26 cs.LO
Well-Definedness and Efficient Inference for Probabilistic Logic Programming under the Distribution Semantics
University of Ferrara（费拉拉大学）；Universidade Nova de Lisboa（新里斯本大学）
分布语义是逻辑程序设计与概率论相结合的重要途径之一。许多语言遵循这种语义，例如独立选择逻辑、PRISM、pD、带有注释析取的逻辑程序（LPAD）和ProbLog。当程序包含函数符号时，只有当查询的解释集是有限的并且每个解释也是有限的时，分布语义才是定义良好的。良好定义通常要么是明确强加的，要么是通过严格限制允许程序的类别来实现的。在本文中，我们确定了一个更大的类的程序，其中的语义是定义良好的计算查询的概率与一个有效的程序。由于LPAD提供了最一般的语法，我们提出了我们的结果，但我们的结果适用于所有的语言下的分布语义。我们提出的算法“概率推理与制表和答案包容”（PITA），计算概率的查询转换成一个正常的程序，然后应用SLG决议与答案包容。PITA已经在XSB中实现，并在六个域上进行了测试：两个域带有函数符号，四个域没有。与ProbLog，cplint和CVE的执行时间相比，PITA几乎总是能够在更短的时间内解决更大的问题，无论是否有函数符号。
2011-10-04 cs.AI cs.LO cs.PL
Parallel Logic Programming: A Sequel
Università di Udine（乌迪内大学）；GNCS-INdAM（意大利国家高等数学研究院-国家科学计算小组）；University of Texas at Dallas（德克萨斯大学达拉斯分校）；IMDEA Software Institute（IMDEA 软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）；New Mexico State University（新墨西哥州立大学）；CRACS/INESC TEC（CRACS/INESC TEC 研究所）；University of Porto（波尔图大学）
多核和高度连接的架构已经变得无处不在，这带来了新的兴趣，基于语言的方法来开发并行性。逻辑程序设计自诞生以来就被认为是一种具有巨大潜力的并行性自动开发的编程范式。2001年出版的对并行逻辑编程前二十年研究的全面调查，一直是研究人员和开发人员的基本参考。这些内容在今天是相当有效的，但与此同时，该领域在随后的几年中继续快速发展。这些成就和正在进行的研究中有许多是由技术创新的快速步伐推动的，这导致了诸如超大型集群、多核处理器的广泛普及、通用图形处理单元的游戏规则改变作用以及云计算的普遍采用等进步。这已经被逻辑编程中的重大进步所证实，例如制表、更强大的静态分析和验证、应答集编程的快速增长，以及一般来说，更成熟的实现和系统。本次调查提供了自2001年以来的并行逻辑编程研究的回顾，从而提供了前一次调查的自然延续。该调查的目标是不仅作为逻辑编程系统的研究人员和开发人员的参考，而且作为对逻辑感兴趣的任何人的引人入胜的阅读，并作为逻辑编程之外的并行系统研究人员的有用资源。逻辑程序设计理论与实践（TPLP）
2022-01-24 cs.AI cs.DC cs.LO
Top-down and Bottom-up Evaluation Procedurally Integrated
本文描述了XSB如何结合自顶向下和自自底向上的【形】的计算，通过不同的制表和包容制表与抽象的机制，分别。众所周知，Prolog中逻辑规则的自顶向下求值具有递归过程调用的过程解释（Kowalski 1986）。Tabling增加了短路冗余计算的直观性（Warren 1992）。本文展示了如何在表逻辑程序评估中引入一个自自底向上的【形】的组件，其过程直观性是数据结构的初始化，其中一个关系在第一次需要时被初始计算和填充，然后在更大计算的剩余部分中用于有效查找。这使得许多Prolog程序可以完全声明地表达，以前需要过程特性（如断言）的程序变得高效。本文正在考虑接受“逻辑程序设计理论与实践（TPLP）”。
2018-04-23 cs.LO
A Theoretical Study of (Full) Tabled Constraint Logic Programming
表格约束逻辑编程（TCLP，tableed constraint logic programming）已经被证明比LP、CLP或LP with tabling更有表现力，在某些情况下更有效。在本文中，我们提供了关于语义，正确性，完整性和终止的自顶向下执行策略的完整TCLP，即，TCLP的特点是在呼叫和应答中进行蕴涵检查。我们提出了一个自顶向下的语义TCLP，并表明它是等价的不动点语义。我们研究了一个程序生成的约束如何有效地影响终止，即使是约束类，约束不紧，概括以前的结果。我们还介绍了不同的约束投影的变体如何影响TCLP实现的正确性和完整性。所有提出的特点都实现（或可以实验）在Mod TCLP，一个模块化的框架表约束逻辑编程，Ciao Prolog逻辑编程系统的一部分。
2020-09-28 cs.LO
Description, Implementation, and Evaluation of a Generic Design for Tabled CLP
具有制表和约束的逻辑编程（TCLP，表格约束逻辑编程）已被证明比LP，CLP或LP +制表更具表达力，在某些情况下更有效。以前的设计TCLP系统没有充分利用蕴涵，以确定呼叫/应答包容，并没有提供一个简单的和良好的记录接口，以促进现有的制表系统中的约束求解器的集成。我们研究的作用，投影和蕴涵在终止，健全和完整的TCLP系统，并提出了设计和实验评估的Mod TCLP，一个框架，简化了额外的约束求解器的集成。Mod TCLP将约束求解器视为制表系统的客户端，这是通用的w.r.t.解决方案，只需要一个明确的接口，从后者。我们通过整合四个约束求解器来验证我们的设计：以前存在的用于差分约束的约束求解器，用C编写; Holzbaur的CLP（Q）和CLP（R）的标准版本，用Prolog编写;以及有限格上的方程的新约束求解器。我们使用上述约束求解器在几个基准测试中评估我们的框架的性能。Mod TCLP是在Ciao Prolog中开发的，Ciao Prolog是一个健壮、成熟的下一代Prolog系统。逻辑程序设计理论与实践（TPLP）
2018-09-15 cs.LO cs.PL
Induction of Non-monotonic Logic Programs To Explain Statistical Learning Models
The University of Texas at Dallas（德克萨斯大学达拉斯分校）
我们提出了一个快速的和可扩展的算法，从统计学习模型诱导非单调逻辑程序。我们减少了搜索最佳条款的高效用项目集挖掘（HUIM）问题的实例的问题。在HUIM问题中，特征值和它们的重要性分别被视为事务和效用。我们利用TreeExplainer，可解释的AI工具SHAP的快速和可扩展的实现，从集成树模型中提取局部重要特征及其权重。我们的实验与UCI标准的基准表明，显着改善的分类评估指标和运行时间的训练算法相比，ALEPH，一个国家的最先进的归纳逻辑程序设计（ILP）系统。
2019-09-18 cs.AI cs.LG cs.LO
Neuro-Symbolic Learning for Predictive Process Monitoring via Two-Stage Logic Tensor Networks with Rule Pruning
University of Parma（帕尔马大学）；Eindhoven University of Technology（埃因霍温理工大学）
本文提出一种神经符号学习方法，通过两阶段优化策略结合逻辑张量网络与规则剪枝，提升预测过程监控的准确性，尤其在合规约束下表现优异。
2026-03-27 cs.AI
A Homogeneous Reaction Rule Language for Complex Event Processing
RuleML Inc.（RuleML公司）；Betfair Ltd.（必发有限公司）；National Research Council（加拿大国家研究委员会）
在当今分布式面向服务的体系结构和基于Web的事件驱动环境中，对复杂事件处理的反应性功能进行事件驱动的自动化是一个迫切的需求。要解决的一个重要问题是如何正确和有效地捕获和处理反应规则中体现的基于事件的行为、反应逻辑，并将其与体现的其他条件决策逻辑相结合，例如，在派生规则中。本文阐述了一种同构集成方法，结合派生规则，反应规则和其他规则类型，如完整性约束到逻辑编程的一般框架，声明式编程的工业强度版本。我们描述的语言的语法和语义，实现一个分布式的基于Web的中间件，使用企业服务技术，并说明其充分的表现力，效率和可扩展性，通过从工业用例中提取的例子。开发的反应规则语言提供了表达功能，如模块化的基于ID的更新，支持外部进口和自我更新的内涵和外延的知识库，交易，包括完整性测试和回滚的更新过渡路径。它还支持分布式复杂事件处理，事件消息传递和事件查询，通过有效的和可扩展的企业中间件技术和事件/动作推理的基础上的事件/动作代数实现的一个基于区间的事件演算变体作为逻辑推理形式主义。
2010-08-04 cs.AI
Distinguishing between Communicating Transactions
通信事务是一种分布式的、非隔离的事务，它为构建并发系统提供了一个简单的结构。在本文中，我们开发了一个逻辑框架来表达这些系统的可观察行为的属性。这包括三个名义模态逻辑，它们共享标准通信模态，但具有不同的涉及事务提交的过去和未来模态。所有这三种逻辑对系统具有相同的区分能力，因为它们相关的弱互模拟与上下文等价一致。此外，它们同样具有表达性，因为它们的公式之间存在语义保持翻译。使用逻辑，我们可以清楚地展示微妙的例子不等价。这项工作提出了第一个属性逻辑的非隔离事务。
2018-01-12 cs.LO
Reasoning about Weak Isolation Levels in Separation Logic
本文针对工业级数据库默认弱隔离级别存在隔离性错误但缺乏可执行实现推理模型的问题，在分离逻辑中形式化读未提交、读已提交和快照隔离三个弱隔离级别，验证其规范可禁止违规执行、可实现且存在蕴含关系。
2025-08-20 cs.LO cs.PL
Forex Trading Robot Using Fuzzy Logic
本研究提出基于模糊Mamdani系统与投票机制的外汇交易机器人，替代传统振荡指标策略，显著提升盈利因子并优化交易准确性。
2025-07-08 cs.CE cs.LO cs.SY
GLP: A Grassroots, Multiagent, Concurrent, Logic Programming Language for AI (Full Version)
London School of Economics（伦敦政治经济学院）；Weizmann Institute of Science（魏茨曼科学研究所）
提出草根逻辑程序（GLP），一种用于实现草根平台的多智能体并发逻辑编程语言，通过多智能体操作语义证明其草根性，并展示其在社交图等平台的应用。
2026-07-07 cs.CR cs.DC cs.LO
A formal model for ledger management systems based on contracts and temporal logic
Sapienza University of Rome（罗马第一大学）；University of Molise（莫利塞大学）
针对当前智能合约易有漏洞、语义偏离法律合约的问题，提出基于有限状态自动机的合约形式化模型，并以时态逻辑构建适配账本历史属性的抽象查询语言，提升账本系统可靠性。
2021-09-30 cs.CL cs.CR cs.LO
Static Application-Level Race Detection in STM Haskell using Contracts
编写并发程序是一项艰巨的任务，即使使用高级同步原语（如事务存储器）和具有良好控制副作用的函数式语言（如Haskell），因为进程之间产生的干扰可能发生在不同的级别，并且以非常微妙的方式发生。当线程将共享数据保留或公开为与应用程序逻辑或数据的真实含义不一致的状态时，就会出现问题。在本文中，我们建议将合同与交易相关联，并定义了一个程序转换，使得在STM Haskell的上下文中扩展静态合同检查成为可能。因此，我们能够静态地检查STM Haskell程序的每个事务处理共享数据的方式，即以用户定义的布尔函数的形式表示的给定一致性属性被保留。这确保了在并发程序的执行过程中不会发生不良干扰。
2013-12-10 cs.DC cs.LO cs.PL
Towards Approximate Query Enumeration with Sublinear Preprocessing Time
本文的目的是提供非常有效的算法近似查询枚举稀疏数据库，性能和准确性的保证。本文提出了一种新的有界度关系数据库类的近似查询枚举模型。我们首先证明了在有界度的数据库上，任何局部一阶可定义查询在经过一个常数时间的预处理阶段后，都可以近似地以常数延迟被枚举。我们扩展这一点，表明在有界树的宽度和有界度的数据库，每一个查询，是在一阶逻辑表达可以枚举近似恒定延迟后，一个次线性（更准确地说，多对数）时间预处理阶段。Durand和Grandjean（ACM Transactions on Computational Logic 2007）证明了在有限度数据库上的一阶查询的精确枚举可以在线性时间预处理阶段之后以恒定延迟完成。因此，我们在预处理阶段实现了显著的加速。由于次线性运行时间不允许读取整个输入数据库，即使是一次，牺牲一些准确性是不可避免的，我们的速度。然而，我们的枚举算法有保证：以高概率，（1）只有元组被枚举是查询的答案或“接近”是查询的答案，（2）如果元组的比例是查询的答案是足够大的，那么所有的答案将被枚举。在这里，“接近度”的概念是输入数据库中的元组编辑距离。对于本地一阶查询，只枚举实际答案，加强了（1）。此外，（2）中所要求的“接近度”和比例都是可控的。我们结合的方法，从属性测试的有界度图的逻辑和查询枚举，我们相信可以激发进一步的研究。
2021-01-15 cs.DB cs.LO
