Regression verification of unbalanced recursive functions with multiple calls (long version)
给定两个程序$p_1$和$p_2$，通常是同一程序的两个版本，回归验证的目标是在给定等价定义的情况下，标记来自$p_1$和$p_2$的等价函数对。最常见的定义是部分等价，也就是说，如果两个函数被输入相同的输入，并且它们都终止，则它们发出相同的输出。回归验证工具（RVT）使用的策略是在$P_1,P_2$的调用图上自自底向上的进行，抽象那些已经被证明与未解释函数等价的函数，将循环转换为递归，并抽象递归调用。这使它能够以无循环和无递归的小程序的形式创建验证条件。只要递归函数是同步的，此方法就能很好地工作，否则通常会失败。在这项工作中，我们研究的问题证明等价时，两个递归函数不同步。有效地，我们扩展以前的工作，研究这个问题的功能与一个单一的递归调用网站，一般情况下。我们还介绍了一种方法，用于自动检测展开，这是必要的两个递归函数同步时，可能的。我们展示了具有多个递归调用的函数对的示例，这些函数对现在可以用我们的方法证明是等效的，但不能用任何其他自动验证系统证明是等效的。
2022-07-28 cs.LO
First-Order Quantification over Automata
针对无限字模型上全称量化依赖补全自动机的难题，本文提出直接计算一元编码自然数公式中全称一阶量词对自动机影响的算法，以支持多种算术理论的可实现判定过程。
2023-06-07 cs.LO
The role of logical interpretations in program development
代数规格说明的逐步精化是程序开发的一种著名的形式化方法。然而，传统的概念，细化的基础上签名态射往往过于僵化，以捕捉一些相关的软件设计，重用和适应的背景下的转换。本文提出了一种新的加细方法，在这种方法中，签名态射被逻辑解释所取代，作为证明加细的一种手段。该方法首先在方程逻辑的背景下，后来推广到任意维度的演绎系统。这允许，例如，细化成方程式规格和后者到模态的。
2014-01-29 cs.LO
A logical framework to model software development by multiple agents following a common specification
针对多主体遵循共同规范但在不同环境下开发的程序的可翻译性问题，扩展用于描述相对主义科学理论建构的逻辑框架，使其可推理程序、生成迭代过程与规范，定义了程序生成器输出间的翻译并证明可靠遵循同规范时存在平凡翻译。
2022-11-02 cs.LO
A logical analysis of entanglement and separability in quantum higher-order functions
我们提出了一个函数量子计算语言的逻辑可分性分析。这种逻辑的灵感来自于以前的作品的逻辑分析别名的命令式函数程序。这两种分析有着显著的相似之处，因为它们都是高度非组合的。量子设置更难处理，因为它引入了非确定性，从而大大修改了逻辑断言的语义和有效性。这种逻辑是纠缠/可分性分析的第一个建议，处理功能量子程序设计语言与高阶功能。
2008-01-04 cs.LO
Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
National and Kapodistrian University of Athens（雅典国立卡波迪斯特里安大学）；University of Ioannina（约阿尼纳大学）
有序析取逻辑程序是对经典逻辑程序的扩展，它具有在程序规则头部表示优先析取的能力。LPOD的初始语义虽然简单且非常直观，但并不是纯粹的模型理论。这样做的后果是，程序的某些属性似乎不平凡的形式化在纯粹的逻辑术语。这种情况的一个例子是LPOD强等价概念的特征。虽然Faber等人（2008）的结果是准确的，但它们没有将LPOD的强等价性表征为某些特定逻辑中的逻辑等价。这与经典逻辑程序的强等价性的著名特征形成了鲜明的对比，正如Lifschitz等人（2001）所证明的那样，强等价性与这里和那里的逻辑中的逻辑等价性相一致。在本文中，我们得到了一个纯粹的逻辑刻画的强等价的LPODs的逻辑等价在一个四值逻辑。此外，我们提供了一个新的证明的coNP-完备性的强等价的LPODs，有兴趣在自己的权利，因为它依赖于这种程序的特殊结构。我们的研究结果是基于Charalambidis等人（2021）介绍的LPODs的最新逻辑语义，我们认为这一事实表明，这种新的语义可能会被证明是LPODs进一步研究的有用工具。
2022-05-10 cs.AI cs.LO
Recursive Session Logical Relations
程序等价是程序性质推理和证明的支点。对于不干扰，例如，程序等价的保密水平的观察员。逻辑关系是这种证明的有力推动者。逻辑关系直到最近才被用于会话类型--但仅用于终止语言。本文将逻辑关系扩展到递归会话类型。它为线性会话类型的进度敏感非干扰开发了一个逻辑关系，解决了非终止和并发带来的挑战。这些贡献包括安全多态过程和与元理论的逻辑关系。一个显着的特点是选择的“步骤指数”的逻辑关系，允许传递性和可靠性的自然证明。
2022-08-30 cs.LO cs.PL
On The Metric Nature of (Differential) Logical Relations
本文阐明了微分逻辑关系的度量本质，证明其产生的拟拟度量可与拟度量和偏度量相关联，并借此推导出关于程序差异的新的组合推理原则。
2025-05-02 cs.LO
Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
本文提出基于SMT求解和模型投影的量词消去算法，解决含不可计算符号的单次调用无递归函数综合问题，并在Z3上实现原型验证其效率。
2025-08-18 cs.LO
On the Metric Nature of (Differential) Logical Relations
University of Bologna（博洛尼亚大学）；INRIA Sophia Antipolis（索菲亚-安提贝斯国家信息与自动化研究所）；Sojo University（昭和大学）；Université Claude Bernard Lyon 1（里昂第一大学）
本文研究微分逻辑关系的度量性质，引入准准度量和微分预逻辑关系，探讨其在程序距离中的应用与特性。
2026-03-01 cs.LO
Normal Nested Answer Set Programs: Syntactics, Semantics and Logical Calculi
本文定义了正规嵌套程序（NNP）的语法、语义及嵌套逻辑演算，填补了嵌套回答集程序推理能力的空白，并证明了相关计算复杂性。
2025-04-07 cs.LO
Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
程序模块理论对语言设计者来说很有意义，不仅因为它对编程的实际重要性，还因为它是语言设计中三个基本问题的联系：阶段区分，计算效果和类型抽象。我们贡献了一个新的“合成”采取程序模块，将模块作为基本的结构，在通常的嫌疑人之前的模块演算（种，构造函数，动态程序）呈现为派生概念的模态类型理论帐户的阶段区别。我们简化了类型抽象的帐户（体现在模块函子的生成性）通过一个松散的模态，封装计算效果。我们的主要结果是程序模块演算的雷诺兹抽象定理的（重要的）证明相关和相敏的推广，基于一种称为参数结构的新型逻辑关系。参数化结构将经典参数化的证明无关关系推广到证明相关的家族，其中可能有非平凡的证据证明两个程序的相关性-简化了类型集合上的强和的元理论，因为虽然不可能有“关系分类关系”，但很容易容纳“家族分类小家族”。使用的洞察力，逻辑关系/parametricity本身是一种形式的语法和语义之间的相位区分，我们贡献了一个新的综合方法相分离parametricity的口号“逻辑关系作为类型”的基础上，迭代我们的模态帐户的相位区分。然后，要在一个抽象类型的两个实现之间构造一个模拟，只需编写第三个实现，其类型组件携带表示不变量。
2021-05-14 cs.LO cs.PL
Non-idempotent intersection types in logical form
交集类型是分析函数式程序和非函数式程序的运算和指称性质的重要工具。其中，非幂等交集类型提供了有关术语和程序评估的精确定量信息。然而，与简单类型或二阶类型不同，交集类型不能被认为是一个逻辑系统，因为应用规则（或交集规则，取决于系统的表示）涉及一个条件，表示前提的证明满足一个非常强的一致性条件：底层的条件项必须相同。使用早期的工作引入索引版本的线性逻辑，我们表明，非幂等类型可以给出一个逻辑形式的系统中，公式表示遗传索引家庭的交叉类型。
2019-11-05 cs.LO
Second-Order Functions and Theorems in ACL2
SOFT ('Second-Order Functions and Theorems') is a tool to mimic second-order functions and theorems in the first-order logic of ACL2. Second-order functions are mimicked by first-order functions that reference explicitly designated uninterpreted functions that mimic function variables. First-order theorems over these second-order functions mimic second-order theorems universally quantified over function variables. Instances of second-order functions and theorems are systematically generated by replacing function variables with functions. SOFT can be used to carry out program refinement inside …
2015-09-21 cs.LO
A Logical Charaterisation of Ordered Disjunction
Corunna University（科伦纳大学）
本文讨论了Brewka、Niemelä和Syrjänen在他们的有序析取逻辑程序（LPOD）中引入的有序析取算子x的逻辑处理。LPOD用于在回答集语义下表示逻辑编程中的偏好。它们的语义是通过首先将LPOD翻译成一组正常程序（称为分裂程序），然后在这些分裂程序的答案集之间施加偏好关系来定义的。我们集中在第一步，并显示如何适当的翻译有序析取作为一个派生的操作符到逻辑的这里和那里允许捕获的答案集的分裂程序在一个直接的方式。我们使用这种特性不仅为LPODs提供了一种替代实现，而且还检查了“x”算子的几个属性（在强等价变换下），例如，其关于合取或正则析取的分布性。我们还比较了Kärger，Lopes，Olmedilla和Polleres提出的扩展，它结合了“x”与定期析取。
2010-11-22 cs.AI cs.LO
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
我们展示了如何自动工具的验证线性和分支的时间属性的程序，多线程，和功能的程序，以及程序合成可以自然地和统一地被视为求解器的约束条件的形式（量化）霍恩条款的背景逻辑理论。这样的观点可以提供各种优势，例如。例如，在一个实施例中，约束生成（也称为证明义务的生成）和约束求解（也称为证明发现）之间的关注点的逻辑分离、跨不同验证任务的求解器的重用、以及证明设计者从低级算法关注点中解放出来，反之亦然。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-29 cs.LO
Scenes: A Meta-Logical Algebra for Mutable State
University of York（约克大学）；University of Aarhus（奥胡斯大学）
本文提出场景（scene）代数结构，用于刻画状态空间中的变量集，支持基于透镜的元逻辑属性分析，并无需语法即可表征自由/约束变量，进而推导并行组合的推理原则。
2026-09-25 cs.LO
Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
本文提出参数化动态逻辑DLp，通过引入程序配置标签支持符号执行与语法结构推理，构建循环预证明系统保证无限证明树可靠性，为通用程序规约与验证提供灵活框架。
2025-01-29 cs.LO cs.SE
Relational Linear Programs
TU Dortmund University（多特蒙德工业大学）；University of Bonn（波恩大学）
我们提出了关系线性规划，一个简单的框架结合线性程序（LP）和逻辑程序。关系线性规划（relational linear program，RLP）是一个声明性的LP模板，通过对象、关系和量化变量的逻辑概念定义目标和约束。这使得人们可以表达LP目标和约束关系的不同数量的个人和他们之间的关系，而不列举他们。连同逻辑知识库，有效地由逻辑事实和规则组成的逻辑程序，它归纳出一个基础LP。使用提升线性规划来求解该基础LP。也就是说，如果可能的话，采用地面LP内的对称性来降低其维数，并且使用任何现成的LP求解器来求解简化的程序。与主流LP模板语言（如AMPL）相比，它具有声明式和命令式编程风格的混合，RLP的关系性质允许在关系域上更直观地表示优化问题。我们说明了这一经验的实验近似推理在马尔可夫逻辑网络使用LP松弛，解决马尔可夫决策过程中，集体推理使用LP支持向量机。
2014-10-12 cs.AI cs.LO cs.PL
Logic programming beyond Prolog
逻辑程序是一种可执行的规范。例如，合并排序在纯Prolog中是一个逻辑公式，但在长链表上显示出值得信赖的性能。但这种可执行的规范是一种妥协：逻辑被算法考虑扭曲，但只能通过抽象机器间接执行。本文介绍了关系编程，一种通过关注点分离解决逻辑编程困难的方法。它需要三个文本：（1）公理，一个指定问题并且不受算法考虑影响的逻辑公式，（2）定理，一个表达算法思想并遵循公理的逻辑公式，以及（3）代码，将定理转录为过程语言。代码的正确性依赖于定理与公理的逻辑关系，并依赖于定理到过程语言的准确转录。排序是关系编程具有更高抽象度优势的一个例子：要排序的数据可以是C++（我们在示例中使用的过程语言）中满足线性顺序公理的任何数据类型，而纯Prolog版本仅限于链接单元格形式的数据结构。我们展示了关系程序的另一个优点：它们具有模型理论和不动点语义，它们彼此等价，并且类似于纯Prolog程序。
2015-09-26 cs.LO cs.PL
DeepLogic: Towards End-to-End Differentiable Logical Reasoning
Imperial College London（帝国理工学院）
将机器学习与基于逻辑的专家系统相结合，以获得两个世界的最佳效果，正变得越来越流行。然而，机器学习在多大程度上可以学习基于规则的知识进行推理仍然是一个悬而未决的问题。在本文中，我们将探讨如何符号逻辑，定义为逻辑程序在字符级别，学习表示在一个高维向量空间使用基于RNN的迭代神经网络进行推理。我们创建了一个新的数据集，定义了12类逻辑程序，举例说明增加了逻辑推理的复杂性，并以端到端的方式对网络进行训练，以了解逻辑程序是否需要给定的查询。我们分析了如何学习推理算法产生的原子，文字和规则的表示在逻辑程序和评估对增加长度的谓词和常量符号，以及增加多跳推理的步骤。
2019-03-07 cs.AI cs.LO cs.NE
A Logical Characterization of the Preferred Models of Logic Programs with Ordered Disjunction
National and Kapodistrian University of Athens（雅典国立卡波季斯特里安大学）
有序析取逻辑程序（LPODs）是对经典逻辑程序的扩展，它能够在程序规则的头部以递减的优先度表示备选项。尽管有序析取的操作意义是明确的，但关于其语义仍存在一个重要的问题。具体地，不存在用于确定LPOD的最优选模型的纯模型理论方法。目前，选择最优选的模型是使用一种技术来执行的，该技术并不完全基于程序的模型，并且在某些情况下会产生违反直觉的结果。我们提供了一个新的，模型理论的语义LPODs，它使用一个额外的真值，以确定最首选的模型的程序。我们证明，所提出的方法克服了传统的语义LPODs的缺点。此外，新的方法可以用来定义一个自然类的逻辑程序，可以有有序的和经典的析取子句的头部的语义。这使得程序不仅可以表达严格的偏好级别，还可以表达同样偏好的替代方案。这项工作正在考虑接受在TPLP。
2021-08-07 cs.AI cs.LO cs.PL
Implementing program extraction from CL1-proofs
可计算性逻辑（Computability Logic，CoL）是一种交互计算的形式化理论。它将计算问题理解为两个玩家的游戏：机器和它的环境，使用逻辑形式主义来描述有效的可计算性原则和公式来表示计算问题。逻辑CL1是CoL的一个片段的演绎系统，逻辑词汇表包含了经典逻辑的所有算子和选择算子，原子表示经典逻辑的基本博弈即谓词。在本文中，我们提出了一个程序，采取CL1证明的任意公式$F$，并提取一个获胜的策略，$F$从证明，然后发挥$F$使用该策略。我们希望本文将提供一个起点，进一步的工作，在程序提取的CoL为基础的算法和其他CoL为基础的应用系统。
2013-11-26 cs.LO
Bialgebraic Reasoning on Higher-Order Program Equivalence
针对高阶程序上下文等价性推理需逐场景构建逻辑关系的问题，本文在高阶数学操作语义框架下提出步索引逻辑关系的通用构造，证明弱操作模型为松弛双代数时逻辑关系自动可靠，且可实例化到多种演算与等价性场景。
2024-05-16 cs.LO cs.PL
Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
University of Toronto（多伦多大学）；Vector Institute（向量研究所）
综合实现逻辑规范的程序是计算机科学中的经典问题。我们研究了一种特殊类型的程序合成，其目标是合成一种策略，该策略对潜在的敌对环境做出反应，同时确保所有执行满足线性时序逻辑（LTL）规范。不幸的是，通过逻辑推理解决所谓的LTL合成的精确方法不具有规模。在这项工作中，我们铸造LTL合成作为一个优化问题。我们采用了一个神经网络学习Q函数，然后用来指导搜索，并构建程序，随后验证的正确性。我们的方法在将搜索与深度学习相结合以实现LTL合成方面是独特的。在我们的实验中，学习的Q-函数提供了有效的指导与相对较小的规格的综合问题。
2019-12-31 cs.AI cs.FL cs.GT
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
2021-07-20 cs.LO cs.PL
Logic of fusion
论文利用 Curry-Howard 同构将程序融合对应于切消除，并借助超自然变换重新解释参数化性，从而逻辑分析各类归纳与共归纳数据类型上的 build 融合。
2020-07-30 cs.LO math.CT
Logical Concurrency Control from Sequential Proofs
我们感兴趣的是识别和执行并发程序的隔离要求，即，确保程序满足其规范的并发控制。本文的论点是，这可以从顺序证明开始系统地进行，即，在没有并发交织的情况下证明程序的正确性。我们说明我们的论文提出了一个解决方案的问题，使一个顺序库线程安全的并发客户端。我们考虑一个顺序库注释断言以及证明这些断言在顺序执行。我们展示了如何使用证明来导出并发控制，以确保库方法的任何执行在由并发客户端调用时满足相同的断言。我们还提出了一个扩展，以保证库方法是线性化或原子。
2011-09-01 cs.LO cs.PL cs.SE
The Logic of Quantum Programs
我们提出了一个逻辑演算推理量子程序中的信息流。特别是，我们介绍了一个动态的逻辑，能够处理量子测量，幺正演化和纠缠的复合量子系统。我们给出了一个语法和关系语义，我们抽象远离阶段和概率。我们提出了一个健全的证明系统，这种逻辑，我们展示了如何通过逻辑手段表征各种形式的纠缠（如贝尔态）和各种线性算子。作为一个例子，我们简要分析了隐形传态协议。
2021-09-14 cs.LO quant-ph
Mixed Logical and Probabilistic Reasoning for Planning and Explanation Generation in Robotics
The University of Auckland（奥克兰大学）
机器人在复杂的领域中帮助人类，必须在感觉运动水平和社会水平上代表知识和理性。本文所描述的架构耦合的非单调逻辑推理能力的声明性语言与概率信念修订，使机器人表示和推理的定性和定量的描述知识和程度的信念。具体来说，不完整的领域知识，包括在所有，但少数例外情况下，持有的信息，表示为一个答案集Prolog（ASP）程序。通过求解该程序获得的答案集用于推理、规划和联合解释（a）由于外源动作引起的意外动作结果和（b）从传感器输入提取的部分场景描述。对于任何给定的任务，答案集中包含的计划中的每个动作都是按概率执行的。自动识别与动作相关的域的子集，并且从传感器输入中提取的观测对在该域子集上定义的置信分布执行增量贝叶斯更新，其中高度可能的置信被提交给ASP程序。该体系结构的能力，说明在模拟和移动机器人的上下文中的机器人服务员在餐厅的餐厅。
2015-08-01 cs.AI cs.LO cs.RO
