Complete Dynamic Logic of Communicating Hybrid Programs
LMU Munich, Germany（慕尼黑大学）；Karlsruhe Institute of Technology, Germany（卡尔斯鲁厄理工学院）；DePaul University, Illinois, USA（德保罗大学）
本文为通信混合程序 dLCHP 提出相对完全的证明演算，通过结合微分动态逻辑 dL 与假设-承诺推理，并借助扩充通信轨迹的 Ω-FOD，证明了并行混合系统推理与混合、连续及离散系统推理难度完全相同。
2026-10-19 cs.LO
Expressiveness of Communication in Answer Set Programming
答案集编程（ASP）是一种声明式编程，允许简洁地制定和有效地解决复杂的问题。这种形式主义的一个直观扩展是通信ASP，其中多个ASP程序协作解决手头的问题。然而，通信ASP的表现力还没有得到彻底的研究。在本文中，我们提出了一个系统的研究提供了额外的表现力，允许ASP程序进行通信。首先，我们考虑一种简单的通信形式，其中程序只允许相互提问。在大多数情况下，我们故意只考虑简单的程序，即程序的计算答案集是在P.我们发现，决定是否是一个文字在一些答案集的通信ASP程序使用简单的通信的问题是NP难的。换句话说：由于这些简单的ASP程序的通信和协作能力，我们在多项式层次结构中向上移动了一步。其次，我们修改了通信机制，使我们能够专注于一系列通信程序，其中序列中的每个程序可能会相继删除一些剩余的模型。这模仿了一个领导者网络，第一个领导者有第一个发言权，可以删除他或她认为不满意的模型。使用这种特殊的通信机制使我们能够捕获整个多项式层次结构。这意味着，特别是，通信ASP可以用来解决的问题，在第二层的多项式层次结构，如某些形式的溯因推理以及PSPACE完全的问题，如CNOPS规划。
2011-09-12 cs.LO cs.PL
HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
针对混合通信顺序进程（HCSP）建模的混合系统，提出基于混合霍尔逻辑的自动定理证明器HHLPar，通过符号分解、同步组合规范及集成外部求解器实现自动验证，经Isabelle/HOL形式化确保可靠，简化巡航控制系统实验验证了其性能。
2025-11-12 cs.LO
Static Analysis of Communicating Processes using Symbolic Transducers
我们提出了一个通用模型，允许静态分析的基础上抽象的解释系统的通信过程。我们的技术受到常规模型检验的启发，将程序状态集表示为格自动机，将程序语义表示为符号转换器。该模型可以表示进程和通信的动态创建/销毁。使用抽象的解释框架，我们能够提供一个健全的过度近似的系统的可达集，从而使我们能够证明安全属性。我们在一个原型中实现了这种方法，该原型针对C程序的MPI库。
2016-11-27 cs.FL cs.LO cs.SE
A Denotational Semantics for Communicating Unstructured Code
程序设计语言语义的一个重要属性是它们应该是组合的。然而，非结构化的低级代码包含类似goto的命令，这使得很难定义组合语义。在本文中，我们遵循Saabas和Uustalu的思想来构造低层代码。这使我们有可能定义一个基于最少不动点的组合指称语义，以允许使用归纳验证方法。我们捕获的语义通信使用有限的痕迹类似于表示的CSP。此外，我们检查此语义的属性，并给出一个例子，演示了推理的通信和跳转。有了这个语义，我们奠定了基础的证明演算，捕捉两者，非结构化的低级别代码和通信的语义。
2015-03-17 cs.LO cs.PL
The (Lazy) Functional Side of Logic Programming
将逻辑程序转换成功能程序的可能性一直是研究的课题。许多方法的共同点是，原始逻辑程序，为了被翻译，需要被良好地模态化，这导致了这样的共识，即这些程序可以被认为是逻辑程序的“功能部分”。因此，“复杂”逻辑变量、动态选择规则的可能性以及非良模程序的一般属性是逻辑程序的独有特征，这一点已被广泛接受。这并不完全正确，因为其中一些特性在惰性函数式语言中自然存在。我们通过定义一个适用于更广泛的逻辑程序的简单翻译，重新讨论了什么功能是逻辑编程范式所独有的老问题，并证明了目前的界限是不合理的限制。
2000-03-20 cs.LO cs.PL
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
本文提出了一种基于展开/折叠变换规则的程序合成方法，该方法可用于从一个后继者的弱一元二阶理论（WS 1 S）的公式导出可终止的确定性逻辑程序。这种综合方法也可作为WS_（1 S）封闭公式的判定过程的证明方法。我们应用我们的综合方法翻译CLP（WS 1 S）程序到逻辑程序，我们也使用它作为一种证明方法来验证无限状态系统的安全性。
2003-11-27 cs.LO cs.PL
Automated Termination Analysis for Logic Programs with Cut
可终止性是逻辑程序的一个重要性质，也是研究得很好的性质。然而，几乎所有的自动终止分析方法都集中在确定的逻辑程序上，而实际的Prolog程序通常使用cut运算符。本文介绍了一种新的预处理方法，它能自动地将Prolog程序转换成无割的逻辑程序，其中无割程序的终止意味着原程序的终止。因此，在该预处理之后，可以应用用于证明确定逻辑程序的终止的任何技术。我们在我们的终止证明程序AProVE中实现了这种预处理，并成功地进行了广泛的实验。
2010-07-28 cs.LO cs.PL
Building Extensible Program Logics through Effect Handlers
New York University（纽约大学）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）
本文提出基于效应处理程序构建可扩展程序逻辑的方法，从表达性程序逻辑出发，实现模拟多种行为的处理程序并证明其属性以扩展逻辑，还开发关系逻辑，该方法能产生更强推理规则且可扩展。
2026-07-15 cs.LO cs.PL
Nominal Logic Programming
名义逻辑是一阶逻辑的扩展，它为抽象语法的形式化和推理提供了一个简单的基础，模一致的重命名的绑定名称（即α-等价）。本文研究基于名义逻辑的逻辑程序设计。我们描述了一些典型的名义逻辑程序，并发展了这类程序的模型论、证明论和操作语义。除了确保实现的正确行为的兴趣，这些结果提供了一个严格的基础技术分析和推理的名义逻辑程序，我们通过例子说明。
2007-08-20 cs.LO cs.PL
A Survey of the Proof-Theoretic Foundations of Logic Programming
一些形式系统，如归结和最小模型语义，为逻辑编程提供了一个框架。在本文中，我们将调查使用结构证明理论作为替代基础。在过去的35年里，研究人员一直在使用这个基础来将逻辑编程从一阶经典逻辑的根源提升到直觉和线性逻辑的高阶版本。这些更具表现力的逻辑程序设计语言允许捕获有状态计算和丰富形式的抽象，包括高阶编程、模块化和抽象数据类型。术语级绑定是另一种抽象，在证明理论和这些扩展逻辑程序设计语言中，它们都得到了优雅而直接的处理。逻辑编程也激发了证明理论的新成果，例如涉及极性和聚焦证明的成果。这些最新的研究结果提供了一个高层次的手段，呈现前向链和后向链风格推理之间的差异。在证明论中验证逻辑编程也有助于识别它与函数式编程、演绎数据库和模型检验的联系和区别。
2021-10-30 cs.LO cs.PL
LTL Model-Checking for Dynamic Pushdown Networks Communicating via Locks
动态下推网络（Dynamic Pushdown Network，DPN）是一组下推系统（Pushdown Systems，PDS），其中每个进程都可以动态地创建新的PDS实例。DPN是具有（可能是递归的）过程调用和线程创建的多线程程序的自然模型。使用锁扩展DPN允许进程彼此同步。因此，带锁的DPN是一种很好的形式主义，可以对通过锁进行同步的多线程程序进行建模。因此，为带锁的DPN提供模型检验算法是很重要的。在这项工作中，我们认为模型检验的DPN与锁对单索引的LTL属性的形式V fi s. t。fi是在PDS i上解释的LTL公式。我们考虑模型检验问题w.r.t.简单赋值（即，配置是否满足原子命题仅取决于其控制位置和持有的锁）和w.r.t.定期评估（即，满足原子命题的配置集合是配置的规则集合）。我们证明了这些模型检验问题是可判定的。
2016-10-11 cs.LO cs.PL cs.SE
A Logic for Correlating Temporal Properties across Program Transformations
程序转换广泛应用于软件的综合、优化和维护。程序转换的正确性依赖于输入程序的一些重要性质的保持。通过把程序看作Kripke结构，程序的许多有趣的性质可以用时序逻辑来表达。在时序逻辑中，公式在单个程序上解释。然而，为了证明变换的正确性，我们会遇到包含一些子公式的公式，这些子公式在输入程序上解释，而在变换后的程序上解释。出现这种情况的一个例子是验证编译器应用的优化程序转换。在本文中，我们提出了一个逻辑称为时间转换逻辑（TTL）的原因，这样的公式。我们考虑不同类型的原始转换，并提出TTL推理规则。我们的程序转换和时序逻辑运算符的定义是新颖的，在他们使用的布尔矩阵代数。这导致了简洁和建设性的规范。此外，我们使用布尔矩阵代数在一个统一的方式来证明可靠的TTL推理规则。
2012-09-24 cs.LO cs.PL
An Improved Proof-Theoretic Compilation of Logic Programs
在以前的工作中，我们表明，逻辑编程编译可以给出一个通用的抽象逻辑程序设计语言的证明理论的理由，并证明了这种技术的情况下，遗传Harrop公式及其线性变体。编译后的子句本身就是逻辑公式，除了在与它们的头相匹配的原子目标上存在二阶抽象。在本文中，我们重新审视我们以前的结果，以更详细和更充分的逻辑理由，消除这种虚假的抽象。然后，我们改进所得到的技术，以有效地支持模式良好的程序。
2012-10-05 cs.LO cs.PL
Transformation Rules for Locally Stratified Constraint Logic Programs
本文提出了一组带否定的约束逻辑程序的转换规则。我们假设每一个程序都是局部分层的，因此，它有一个唯一的完美模型。我们给出了充分的条件，确保建议的一套转换规则保持完美的模型的程序。我们的规则扩展在某些方面的规则逻辑程序和约束逻辑程序已经考虑在文献中，特别是，他们包括一个规则展开一个条款相对于一个负文字。
2004-02-20 cs.LO cs.PL
Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
本文扩展Outcome Logic，以选择的代数表示统一刻画非确定性、概率性等分支效应，并给出支持通用循环、可跨规范复用证明片段的较完整证明系统及其元理论。
2025-06-10 cs.LO cs.PL
Transforming Coroutining Logic Programs into Equivalent CHR Programs
我们扩展了一种称为编译控制的技术。该技术将协同程序设计逻辑程序转换为逻辑程序，当在标准的从左到右选择规则下执行时（并且不使用任何延迟特征），该逻辑程序具有与协同程序设计相同的计算行为。在最近的工作中，我们修改了编译控制，并将其重新表述为抽象合取部分演绎的实例。这项工作主要集中在编译控制中执行的程序分析。在当前的文件中，我们专注于合成的转换程序。代替合成一个新的逻辑程序，我们合成一个模拟协同程序的Prolog程序。对递归的综合产生只包含简化规则的程序，这些规则特别适合于某些静态分析技术。这些程序也更简洁和可读，并且可以移植到嵌入在其他语言中的Prolog实现。
2017-08-24 cs.LO cs.PL
Tuning Fuzzy Logic Programs with Symbolic Execution
模糊逻辑程序设计是一个不断发展的声明性范例，旨在将模糊逻辑集成到逻辑程序设计中。当指定一个模糊逻辑程序时，最困难的任务之一是确定每个规则的正确权重，以及最合适的模糊连接词和运算符。在本文中，我们介绍了一个符号扩展的模糊逻辑程序，其中一些参数可以是未知的，使用户可以很容易地看到他们可能的价值观的影响。此外，给定多个测试用例，可以自动计算这些参数的最合适的值。
2016-08-16 cs.LO cs.PL
Gödel Logic: from Natural Deduction to Parallel Computation
命题哥德尔逻辑用线性$A\rightarrow B\ \lor\ B\rightarrow A$的非构造性原理扩展了直觉主义逻辑。我们介绍了一个Curry-Howard对应这种逻辑，并表明，一个特别简单的自然演绎演算可以用作一个类型系统。由此产生的函数式语言丰富了简单类型的λ演算与并行进程之间的同步通信机制。我们的规范化证明采用了原始的终止参数和复杂的证明转换与有意义的计算阅读。我们的结果提供了一个计算解释哥德尔逻辑作为一个逻辑的通信并行进程，从而证明了Avron的1991年猜想。
2017-06-18 cs.LO
On completeness of logic programs
程序正确性（在命令式和函数式编程中）在逻辑编程中分为正确性和完整性。完整性意味着一个程序产生了它的规范所要求的所有答案。很少有人致力于对完备性的推理。本文给出了定规划完备性的几个充分条件。我们还研究了在SLD树的某些修剪情况下（例如，由于使用切割）保持完整性。我们将逻辑编程视为一种声明性的范例，尽可能地从任何操作语义中抽象出来。我们认为，所提出的方法是足够简单的应用，可能在一个非正式的水平，在实际的Prolog编程。我们指出近似规格的重要性。
2014-11-11 cs.LO cs.PL
Predicate Specialization for Definitional Higher-order Logic Programs
高阶逻辑编程是传统逻辑编程的一个有趣的扩展，它允许谓词作为参数出现，并在谓词通常出现的地方使用变量。高阶特性确实是理想的，但另一方面，它们的支持通常也更昂贵。在本文中，我们提出了一个程序专业化技术的基础上，部分评估，可以适用于一个温和的，但有用的类高阶逻辑程序，并可以将它们转换为一阶程序，而无需引入额外的数据结构。由此产生的一阶程序可以由传统的逻辑编程解释器执行，并受益于其他可能可用的优化。我们提供了一个实施和实验结果，表明转换的效率。
2018-12-01 cs.LO cs.PL
Logic + control: On program construction and verification
本文提出了一个例子，形式化推理的语义Prolog程序的实际意义（SAT求解器的豪和国王）。该程序被视为一个带有附加控制的定子句逻辑程序。逻辑程序是通过逐步精化的方法构造的，并与其正确性和完整性证明携手并进。证明是声明性的--它们不引用任何操作语义。逻辑程序构造的每一步都遵循一种系统的方法来构造可证明正确和完整的程序。我们还证明了在最终的Prolog程序中保持了逻辑程序的正确性和完整性。此外，我们证明终止，发生检查自由和非挣扎。我们的例子展示了如何将处理“逻辑”和处理“控制”分开。大多数证明都可以在“逻辑”级别上完成，从任何操作语义中抽象出来。这个例子使用了近似的规格说明;它们在简化逻辑程序的推理中是至关重要的。它还表明，语义保持程序转换的范例可能是不够的。我们建议考虑转换保持正确性和完整性方面的近似规范。
2017-05-12 cs.LO cs.PL
The Limits of Horn Logic Programs
给定Horn逻辑程序序列$\{Π_n\}$，$\{Π_n\}$的极限$Π$是这样的子句集合，使得$Π$中的每个子句属于几乎每个$Π_n$，并且无限多个$Π_n$中的每个子句也属于$Π$.极限程序$Π$仍然是Horn，但可能是无限的。本文考虑给定Horn逻辑程序序列$\{Π_n\}$的极限的最小Herbrand模型是否等于每个逻辑程序$Π_n$的最小Herbrand模型的极限。本文证明了这一性质一般不成立，但如果Horn逻辑程序满足一个可语法检验且可由一类Horn逻辑程序满足的假设，则这一性质成立。因此，在此假设下，我们可以通过每个有限程序$Π_n$的最小Herbrand模型序列来逼近极限$Π$的最小Herbrand模型.我们还证明了，如果一个有限Horn逻辑程序满足这个假设，那么这个程序的最小Herbrand模型是递归的。最后，利用动力系统的稳定性概念，证明了这一假设是保证Horn逻辑程序不动点稳定的充分条件。
2002-02-07 cs.LO cs.PL
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
我们提出了一个工具，用于验证的混合系统表示的顺序片段的HCSP（混合通信顺序进程）。该工具允许注释HCSP程序与前，后条件，不变量，并证明规则的推理常微分方程。验证条件是根据混合霍尔逻辑的规则从注释中生成的。我们设计了标记和突出显示机制来区分和可视化不同的验证条件。该工具使用Python实现，并具有基于Web的用户界面。我们评估了翻译的Simulink/Stateflow模型和KeYmaera X基准工具的有效性。
2023-02-21 cs.LO
Verification Logics for Quantum Programs
我们调查景观的霍尔逻辑的量子程序。我们回顾三篇论文：Chadha，Mateus和Sernadas的“Reasoning about imperative quantum programs”; Yoshihiko Kakutani的“A logic for形式化验证of quantum programs”; Mingsheng Ying的“Floyd-霍尔逻辑for quantum programs”。我们比较了逻辑的数学基础，它们的底层语言，以及它们的断言的表达能力。我们还使用这些语言对Deutsch-Jozsa算法进行了验证，并讨论了它们在实际中的相对可用性。
2019-04-08 cs.ET cs.LO cs.PL
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
2008-09-01 cs.AI cs.LO cs.PL
Reachability Analysis of Communicating Pushdown Systems
在可靠的FIFO通道上异步通信的递归程序的可达性分析要求限制以确保可判定性。我们的第一个结果描述了通信拓扑结构的可判定可达性问题，仅限于急切运行（即，消息在发送后立即被接收或从未被接收的情况下运行）。在可判定的情况下，问题是EXPTIME完全的。第二个结果是一个双指数时间算法的有界上下文分析在这种情况下，以及匹配的下限。这两个结果扩展和改进以前的工作从La Torre等人。
2012-09-28 cs.FL cs.LO
Extensional Higher-Order Logic Programming
University of Athens（雅典大学）；University of Victoria（维多利亚大学）
我们提出了一个纯粹的扩展语义高阶逻辑编程。在这个语义中，程序谓词表示有序元组的集合，两个谓词相等当且仅当它们作为集合相等。此外，每个程序都有唯一的最小Herbrand模型，它是程序所有Herbrand模型的最大下界，也是直接结果算子的最小不动点。我们还提出了一个SLD分辨率证明程序，这是证明的声音和完整的最小模型语义。换句话说，我们提供了一个纯粹的扩展的理论框架，高阶逻辑编程的经典（一阶）逻辑编程的熟悉的理论。
2011-06-17 cs.AI cs.LO cs.PL
Characterization of Strongly Equivalent Logic Programs in Intermediate Logics
与逻辑程序的答案集语义相关的非经典、非单调推理关系产生了逻辑程序之间的“强等价”关系，该关系可以在3值Goedel逻辑G3中得到验证，G3是最强的非经典中间命题逻辑（Lifschitz，Pearce和Valverde，2001）。本文将证明KC（通过将公理~A v ~A加到直觉逻辑中而得到的逻辑）是最弱的中间逻辑，对于它，强等价的逻辑程序在允许否定的语言中是逻辑等价的。
2002-06-03 cs.LO
Propositional Dynamic Logic for Message-Passing Systems
我们研究了一个双向命题动态逻辑（PDL）有限和无限消息序列图（MSC）扩展LTL和TLC-。通过这种多模态逻辑，我们可以表达事件的整个未来和过去的属性。路径表达式加强了时态逻辑的经典until算子。对于每个定义MSC语言的公式，我们构造了一个接受相同语言的通信有限状态机（CFM）。得到的CFM在公式的大小上具有大小指数。该合成问题完全一般性地解决，即，也适用于具有无界通道的MSC。CFMs和HMSC的模型检验问题对于存在有界MSC是PSPACE问题。最后，我们表明，对于PDL的交集，公式的语义不能被捕获的CFM了。
2010-09-07 cs.LO
First-Order Modular Logic Programs and their Conservative Extensions
模块化逻辑程序提供了一种将逻辑程序视为由许多独立的、有意义的模块组成的方法。本文介绍了一阶模逻辑程序，它可以捕获许多答案集程序的含义。我们还介绍了保守的扩展，这样的程序。这个概念有助于识别模块化程序之间以及传统程序之间的强关系。我们展示了如何保守扩展的概念可以用来证明常见的投影重写。这篇笔记正在考虑发表在《逻辑程序设计的理论与实践》上。
2017-02-17 cs.LO
Category theoretic semantics for theorem proving in logic programming: embracing the laxness
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数，其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数，描述了归结导子.使用宽松的语义，这种对应关系可以扩展到一类没有存在变量的一阶逻辑程序。由此产生的扩展捕获逻辑编程中的术语匹配分辨率的证明。完善宽松的方法，我们进一步扩展到任意逻辑程序。我们还展示了一个完善的Bonchi和Zanasi的饱和语义逻辑编程，补充宽松的语义。
2016-02-17 cs.LO
Foundations of logic programming in hybrid-dynamic quantum logic
本文提出一种简单且富有表达力的混合动态逻辑用于描述量子程序，研究其中的 Horn 子句并证明初始语义定理，进而通过证明 Herbrand 定理变体奠定了该逻辑片段中量子程序逻辑编程的基础。
2024-06-04 cs.LO
Program Logics for Homogeneous Generative Run-Time Meta-Programming
本文提供了同构生成运行时间元编程的第一个程序逻辑-使用Davies和Pfenning的MiniML变体作为其底层Meta程序设计语言。我们证明了我们的方法的适用性推理的例子元程序从文献。我们还证明了我们的逻辑是相对完整的库克意义上，使归纳推导的特征公式，并准确地捕捉观察属性诱导的操作语义。
2017-03-29 cs.LO
An Almost Classical Logic for Logic Programming and Nonmonotonic Reasoning
介绍了一种称为N^4的一阶逻辑的模型理论。N^4并不像经典逻辑那样消除双重否定，而是减少了四重否定。N^4非常接近经典逻辑：N^4有两个真值; N^4中的蕴涵是实质性的，就像在经典逻辑中一样;否定分布在N^4中的复合公式中，就像在经典逻辑中一样。结果表明，正规逻辑程序的语义可以方便地用N^4形式化：经典逻辑Herbrand解释可以直接推广到N^4;正逻辑程序的经典最小Herbrand模型与其唯一的最小N^4 Herbrand模型一致;正规逻辑程序的稳定模型与其所谓的完全最小N^4 Herbrand模型一致.
2002-07-25 cs.LO
Knowledge Compilation of Logic Programs Using Approximation Fixpoint Theory
出现在逻辑程序设计的理论与实践（TPLP），ICLP 2015会议录知识编译的最新进展介绍了将\emph{positive}逻辑程序编译为命题逻辑的技术，主要是利用最小不动点计算的构造性。这种方法与现有方法相比有几个优点：它保持逻辑等价性，不需要（昂贵的）循环中断预处理或引入辅助变量，并且显著优于现有算法。不幸的是，这种技术仅限于\emph{negation-free}程序。在本文中，我们展示了如何将它扩展到一般的逻辑程序下的良基语义。我们在近似不动点理论中开展工作，这是一个代数框架，它统一了不同逻辑的语义。因此，我们的代数结果也适用于自认识逻辑，缺省逻辑和抽象辩证框架。
2015-07-23 cs.LO
Inconsistency Robustness in Logic Programs
不一致鲁棒性是“信息系统面对持续普遍的不一致时的性能。“不一致鲁棒性的一个基本原则是使矛盾明确，以便支持和反对命题的论点可以形式化。本文探讨了不一致鲁棒性在逻辑程序的历史和理论中的作用。罗伯特·科瓦尔斯基（Robert Kowalski）提出了一个大胆的论点：“回顾我们早期的发现，我最重视的发现是计算可以被演绎所包含。然而，数学逻辑不能总是推断出计算步骤，因为计算系统使用仲裁来确定同时发送多个消息的接收者接下来处理哪个消息。由于接收顺序通常是不确定的，因此不能仅通过数学逻辑从先验信息中推断出它们。因此，数学逻辑一般不能实现计算。随着历史的发展，术语“函数式程序”随着该领域的成熟而变得更加精确和技术化。“逻辑程序“应该也在类似的轨迹上。因此，“逻辑程序“应该具有一般的精确特征。在1972年秋天，逻辑程序的不同特征一直延续到今天：* 逻辑程序使用Horn-Clause语法进行前向和后向链接 * 逻辑程序的每个计算步骤（根据Actor模型）都是演绎推断的（例如在直接逻辑中）。上述示例说明了在逻辑程序中如何反复出现不一致鲁棒性问题。
2015-03-02 cs.LO
Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
该研究证明稳定模型语义下逻辑程序的射影Beth可定义性定理，提出通过一阶Craig插值构造强等价程序的方法，并通过原型实现验证其可行性，推动可定义性与插值方法向回答集编程的迁移应用。
2024-04-28 cs.LO
Logic programs with monotone cardinality atoms
我们研究的MCA程序，即逻辑程序的条款建立的单调基数原子的形式kX，其中k是一个非负整数和X是一个有限的命题原子集。我们发展了一个多学科计算机辅助设计的理论。我们证明了一步可证明性算子的操作概念可以推广到mca-程序，但是推广涉及到不确定性。我们的主要结果表明，MCA程序的形式主义是一个共同的推广（1）正常的逻辑程序设计与其语义的模型，支持的模型和稳定的模型，（2）逻辑程序设计与基数原子和语义的稳定模型，定义的Niemela，Simons和Soininen，（3）析取逻辑程序设计与Sakama和井上的可能模型语义。
2003-10-31 cs.LO
A Logic for Recursive Quantum Programs
大多数现代（经典）程序设计语言都支持递归。递归也被成功地应用于几种量子算法的设计，并被引入到几种量子程序设计语言中。因此，可以预期递归将成为量子编程的基本范式之一。已经开发了几种程序逻辑用于验证非递归量子程序。然而，在量子计算中，还没有通用的方法来推理递归过程。我们填补了空白，本文提出了一个递归量子程序的逻辑。该逻辑是量子While程序的量子霍尔逻辑的推广。证明了该逻辑的（相对）完备性，并通过一个运行的例子：不动点Grover搜索证明了其有效性。
2018-12-10 cs.LO
Incorrectness Logic for Graph Programs
程序逻辑通常会推理程序行为的过度近似，以证明没有错误。最近，程序逻辑已经被提出，而不是证明存在的缺陷，通过下近似推理，这有更好的可扩展性的承诺。在本文中，我们提出了一个下近似的程序逻辑的不确定性图形程序设计语言，并展示了它如何可以被用来推断程序不正确，是否被禁止的图形结构的存在下定义的或由故障执行。我们证明了这种不正确逻辑是健全的和完整的，并推测它的一些可能的未来应用。
2022-03-13 cs.LO
Pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018)
本卷构成了第28届基于逻辑的程序合成和转换国际研讨会的预录（LOPSTR 2018），于2018年9月4日至6日在美因河畔法兰克福举行，德国，并与第20届声明式编程原则和实践国际研讨会同地举行（PPDP 2018）和第26届函数和逻辑编程国际研讨会（WFLP 2018）。
2018-09-11 cs.LO
A program logic for higher-order procedural variables and non-local jumps
依靠经典逻辑的公式即类型范式，我们为具有高阶过程变量和非局部跳转的命令式语言定义了程序逻辑。然后，我们展示了如何为这种程序设计语言导出一个合理的程序逻辑。作为一个副产品，我们得到了一个非依赖类型系统，它比通常在静态类型命令式语言中发现的更宽容。作为一个通用的例子，我们编码了分隔延续操作符shift和reset的命令式版本。
2011-12-07 cs.LO
Graph-based Interpretation of Normal Logic Programs
在本文中，我们提出了一个依赖图为基础的方法来计算正常的逻辑程序的各种语义。我们的方法采用\textit{conjunction nodes}明确表示正常的逻辑程序的依赖图。该依赖图可以以语义保持的方式进行适当的转换，并重新转换为等价的正常逻辑程序。这种转换后的正规逻辑程序可以用回答集编程（ASP）中编写的一些规则来扩充，并使用CLINGO系统来计算其回答集。根据这些附加规则在ASP中的编码方式，可以在稳定模型语义、良基语义或共稳定模型语义下计算原始正常逻辑程序的模型。在每种情况下，也会生成模型中每个原子的对齐。我们报告我们的方法的实施以及其性能评估。
2021-11-25 cs.LO
Coalgebraic Semantics for Probabilistic Logic Programming
本文提出概率逻辑编程的余代数语义，通过函子F的余代数建模程序，并利用余自由余代数给出推导树与可能世界两种语义，可恢复分布语义，并扩展至加权逻辑编程。
2021-04-09 cs.LO
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
本文提出将断言提升至任意状态集合性质的超霍尔逻辑，可在同一框架内证明和否证包括现有逻辑无法表达的任意程序超性质，且已证明其可靠性与完备性，所有结果均在Isabelle/HOL中验证。
2024-04-11 cs.LO
An SMT-Based Concolic Testing Tool for Logic Programs
Concolic测试混合了符号和具体执行，以有效地生成覆盖路径的测试用例。它的好处已经证明了超过15年的测试迫切的程序。其他编程范式，如逻辑编程，受到的关注较少。本文提出了一种基于concolic的逻辑程序测试生成方法。我们的方法利用SMT解决约束决议。然后，我们描述了一个concolic的Prolog测试工具的实现，并验证它在一些选定的基准。
2020-02-17 cs.LO
Hypotheses Founded Semantics of Logic Programs for Information Integration in Multi-Valued Logics
我们解决了整合来自不同来源的信息的问题。信息由中央服务器收集的事实组成，并试图使用（a）一组逻辑规则，即逻辑程序，和（b）表示服务器自己的估计的假设来组合。在这样的设置不完整的信息从一个来源或矛盾的信息从不同的来源需要使用多值逻辑程序可以评估和假设可以测试。为了进行这样的活动，我们提出了一个正式的框架，如贝尔纳普的四值逻辑双格的基础上。在这个框架中，我们的工作与类的程序定义的拟合，我们开发了一个理论的信息集成。我们还建立了一个直观的吸引力之间的连接，我们的假设检验机制，一方面，和有理有据的语义和Kripke-Kleene语义的Datatron程序与否定，另一方面。
2001-11-27 cs.LO
Deriving Program Logics from Distributive Monoidal Categories
Università di Pisa（比萨大学）；Tallinn University of Technology（塔尔图理工大学）；University of Oxford（牛津大学）
该研究从命令式范畴的公理推导多种程序逻辑，其规则遵循该范畴公理，且推导的防护命令代数推广了带测试的防护Kleene代数。
2026-09-04 cs.LO
Termination Proofs for Logic Programs with Tabling
表格逻辑编程在逻辑编程社区中越来越受到关注。它避免了SLD执行的许多缺点，并为逻辑程序提供了一种更灵活且通常非常有效的执行机制。特别地，逻辑程序的表格执行比基于SLD解析的执行更频繁地终止。在这篇文章中，我们介绍了两个概念的通用终止逻辑编程与Tabling：准终止和（更强的概念）LG终止。我们提出了这两个概念的终止，即准可接受性和LG-可接受性的充分条件，我们表明，这些条件也是必要的情况下，制表是精心挑选的。从这些条件出发，我们给出了模终止证明，即，证明能够组合单独程序的终止证明以获得组合程序的终止证明。最后，在模式信息的存在下，我们陈述了充分条件，这些条件构成了以基于约束的方式自动证明终止的基础。
2000-03-09 cs.LO
Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics
本文提出总结果逻辑（TOL），一种统一逻辑，能表达部分与完全正确性等全部终止条件，扩展至非确定性与概率程序，并涵盖现有（不）正确性逻辑分类，实现统一推理。
2025-06-23 cs.LO
An asymptotic analysis of probabilistic logic programming, with implications for expressing projective families of distributions
LMU München（慕尼黑大学）
概率逻辑编程是统计关系型人工智能的重要组成部分，其中将逻辑和概率方法结合在一起，在不确定性环境中推理和学习关系域。然而，跨可变域大小的统计关系表示的行为是复杂的，并且将推理和学习扩展到大型域仍然是一个重大挑战。近年来，域大小依赖、提升推理和从抽样子群体中学习之间出现了联系。统计关系表示的渐近行为已经受到审查，和投影被调查的最强形式的域大小的依赖，其中查询边际是完全独立的域大小。在这篇文章中，我们证明了每一个概率逻辑程序下的分布语义是渐近等价于一个非循环的概率逻辑程序只包括确定条款的概率事实。我们的结论是，每一个概率逻辑程序诱导一个投影族的分布，实际上是处处等价于一个程序从这个片段，我们调查的后果，为投影族的分布概率逻辑程序表示。为了方便应用的经典结果从有限模型理论，我们引入了抽象的分布语义，定义为一个任意的逻辑理论概率事实。这弥合了与概率逻辑编程基础的分布语义之间的差距。在这种表示中，确定性逻辑程序对应于无量词理论，使得渐近量词消去结果可用于概率逻辑编程的设置。本文件正在考虑被TPLP接受。
2021-08-18 cs.AI cs.LO cs.PL
Optimizing Probabilities in Probabilistic Logic Programs
本文提出概率可优化逻辑程序，并给出算法，在满足约束下优化随机变量概率赋值，以解决概率逻辑编程中的概率优化问题。
2021-08-06 cs.LO
Temporal Probabilistic Logic Programs: State and Revision
在许多应用中，我们必须处理与事件相关的时间不确定性。时间概率（TP）逻辑程序应该通过提出不确定时刻的概念来支持事件的有效时间不确定性，即具有相关的上下概率分布的时间点（事件的时间窗）的间隔。特别是，我们提出了新的语义，为TP逻辑程序的Dekhtyar和Subrahmanian。我们的语义，可能的世界语义的基础上，是一个概括的可能的世界语义（非时间）概率逻辑编程，我们定义了新的语法PT程序，明确表示在所有原子的时间变量，并显示如何作为可能的世界概率分布的Herbrand解释的标准作用是连贯地扩展到时间概率逻辑编程。
2011-03-05 cs.LO
