Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees
给定一个逻辑中提出的微积分，一个自然的问题是证明的等价性：以确定是否两个给定的证明是等同的任何指称语义，即任何类别的解释逻辑兼容其削减消除程序。这个概念通常可以通过一组规则排列在语法上捕获。非常一般地，证明网可以被定义为提供证明的等价类的规范表示的组合对象。特别地，逻辑的证明网的存在性提供了该逻辑的等价性问题的解决方案。在线性逻辑的某些片段中，可以给出具有良好计算性质的证明网的概念，使其成为研究割消过程的证明的合适表示。最近已经证明，对于线性逻辑的乘法（有单位）片段，不可能有这样一个证明网的概念，因为这个逻辑的等价问题是P空间完全的。研究线性逻辑中的乘加（无单位）片段，发现它与二进制决策树密切相关：建立了基于二进制决策树的证明表示，将证明等价约化为决策树等价，并给出了二进制决策树的逆编码作为证明.作为我们的主要结果，我们得到的证明等价问题的研究片段的复杂性是对数空间完全的。
2017-11-28 cs.LO
Equilibrium Semantics and Strong Equivalence for Higher-Order Logic Programs
Harokopio University of Athens（哈罗基奥雅典大学）；National and Kapodistrian University of Athens（雅典国立卡波季斯特里安大学）
本文通过扩展均衡逻辑框架为高阶回答集编程建立逻辑语义，证明分层高阶逻辑程序具有唯一均衡模型，并推广强等价性定理。
2026-06-01 cs.LO
Identifying and Explaining (Non-)Equivalence of First-Order Logic Formulas
Ruhr University Bochum（波鸿鲁尔大学）；TU Dortmund University（多特蒙德工业大学）
本文提出了一种基于理论和现有工具的方法，用于测试和解释一阶逻辑公式的等价性，通过大规模实验验证了其有效性。
2026-09-15 cs.LO
Equivalence and Conditional Independence in Atomic Sheaf Logic
University of Ljubljana（卢布尔雅那大学）；Institute of Mathematics, Physics and Mechanics（数学、物理与力学研究所）
本文提出了一种逻辑语义基础，用于在具有变量等价、变量粗等价和变量条件独立性的设置中进行推理。通过原子sheaf拓扑研究了等价与条件独立性的逻辑，并展示了其在经典逻辑中的应用。
2026-05-15 cs.LO math.CT math.LO
A New Game Equivalence and its Modal Logic
我们重新审视自然游戏等价的关键问题，以及基于这些的游戏逻辑的语义。我们提出的原因，调查更精细的概念，游戏等价比平等的标准权力，虽然停留短的模态互模拟。具体地说，我们提出了一个更细粒度的概念平等的“基本权力”，记录什么球员可以强迫加上他们留给别人做，互动的一个重要特征。正如我们详细解释的那样，这个概念更接近于博弈论的战略形式，同时仍然符合逻辑分析。我们通过一个新的表示定理确定基本权力的属性，找到一个匹配的“即时邻居博弈逻辑”，并展示了我们的分析可以扩展到一个新的博弈代数和动态博弈逻辑。
2017-07-27 cs.GT cs.LO
Qualitative Logics and Equivalences for Probabilistic Systems
我们调查的逻辑和等价关系，捕捉定性行为的马尔可夫决策过程（MDP）。我们提出了定性随机CTL（QRCTL）：这种逻辑公式可以表达这样一个事实，即某些时间属性持有所有路径，或概率为0或1，但它们不区分中间概率值。我们提出了一个符号的，多项式时间模型检测算法的QRCTL MDP。逻辑QRCTL在MDP的状态上导出了一个等价关系，我们称之为定性等价：非正式地说，如果两个状态下概率为0或1的公式集相同，则两个状态是定性等价的。我们表明，对于有限的交替MDP，其中不确定性和概率的选择发生在不同的状态，定性等价与交替互模拟相吻合，因此可以通过有效的分区细化算法计算。另一方面，在非交替MDP中，等价关系不能通过划分细化算法来计算，而是需要非局部计算。最后，我们考虑QRCTL*，它以与CTL* 扩展CTL相同的方式用嵌套的时态运算符扩展QRCTL。我们表明，QRCTL和QRCTL* 诱导交替MDP相同的定性等价，而在非交替MDP，从QRCTL* 产生的等价可以严格更精细。我们还提供了一个完整的定性等价，互模拟，交替互模拟之间的关系的表征，根据是否MDP是有限的，以及他们的过渡关系是否是有限分支。
2009-05-04 cs.LO
Strong Equivalence and Program Structure in Arguing Essential Equivalence between Logic Programs
答案集编程是一个突出的声明式编程范式，用于制定组合搜索问题和实现不同的知识表示形式主义。对于一个给定的问题，通常会有几个相关但又有很大不同的答案集程序。有时这些编码可能会显示出显著不同的性能。揭示这些程序之间精确的形式联系通常很重要，但远非微不足道。本文提出了正式的结果仔细有关一些有趣的程序重写。为了提高效率，本文还对系统Projector自动重写程序的正确性进行了证明。逻辑程序设计理论与实践（TPLP）
2021-09-07 cs.AI cs.LO
Strong Equivalence for LPMLN Programs
Arizona State University（亚利桑那州立大学）
LPMLN是一个概率扩展的答案集程序的权重方案改编自马尔可夫逻辑。我们研究了LPMLN中强等价的概念，这是一个有用的数学工具，简化了LPMLN程序的一部分，而不看它的其余部分。我们表明，在LPMLN中的强等价性的验证可以减少到等价性检查，在经典逻辑通过约简和选择规则，以及在“软”逻辑下的等价性检查这里和那里。结果使我们能够利用答案集求解器进行LPMLN强等价性检查。该研究还建议我们使用选择规则，这里和那里的逻辑和经典逻辑的LPMLN语义的一些重新表述。
2019-09-18 cs.AI cs.LO
MALL proof equivalence is Logspace-complete, via binary decision diagrams
逻辑中的证明等价问题是判定两个证明是否模一组规则置换等价的问题，这些规则置换反映了其割消过程的交换转换。因此，它与证明网的问题有关：找到具有良好计算特性的等价证明类的规范代表。它也可以看作是自由范畴概念对应于逻辑的语词问题。最近已经表明，MLL（线性逻辑的单位片段的乘法）中的证明等价是PSPACE-完全的，这排除了这种特定逻辑的证明网的任何低复杂度概念。由于它是另一个片段的线性逻辑，试图定义一个完全令人满意的低复杂度的概念证明网还没有成功，到目前为止，我们研究证明等价MALL-（乘法加法没有单位片段的线性逻辑），并发现一种情况是完全不同的MLL的情况。事实上，我们证明在MALL等价对应（根据AC 0减少）等价的二元决策图，一个数据结构广泛用于表示和分析布尔函数有效。我们证明了这两个等价问题是LOGSPACE完备的。如果这在技术上为MALL-的证明网问题的完整解决方案留下了可能性，那么与二元决策图建立的关系实际上表明了这个问题的否定解决方案。
2015-04-17 cs.LO
Approximations of Isomorphism and Logics with Linear-Algebraic Operators
可逆映射等价是图同构的近似，它改进了著名的Weisfeiler-Leman方法。它们由一个数k和一组素数Q来参数化。直觉是，两个图G和H是等价的关于k-Q-IM-等价不能区分的细化的k-元组的线性算子作用于向量空间上的领域的特征p，任何p在Q。这些等价最早出现在秩逻辑的研究中，但实际上它们可以用来界定任何带有线性代数算子的不动点逻辑扩展的表达能力。定义了特征为p的有限向量空间上的k元线性代数算子无穷逻辑，并证明了k-Q-IM-等价是这种逻辑的初等等价的自然概念.通过对Cai、Fürer和Immerman的CFI-结构的一个广义变体（对于任意素数p）的一个新的和更深入的代数分析，我们证明了：只要Q不是所有素数的集合，就不存在k使得k-Q-IM-等价与同构相同。由此可见，图的多项式时间性质在具有所有Q-线性代数算子和多个变量的无限逻辑中是不可定义的，这意味着具有线性代数算子的不动点逻辑的任何扩展都不能捕获PTIME，除非它包括所有素特征的此类算子。我们的分析需要大量的代数机械，包括一个同质性的CFI结构和Maschke定理，一个重要的结果，从有限群的表示理论。
2019-08-27 cs.CC cs.LO math.LO
Logically automorphically equivalent knowledge bases
知识库理论提供了一个重要的例子，在这个领域中，泛代数和代数逻辑的应用看起来非常自然，它们与计算机科学中出现的实际问题的相互作用可能非常富有成效。本文研究了知识库的等价问题。我们的兴趣是找出信息等价是如何与知识的逻辑描述。研究知识库的各种等价物使我们能够比较不同的知识库。本文的主要目标是逻辑自同构等价的知识库。正如我们将看到的，这个概念为我们提供了一个足够好的知识库特征。
2017-07-04 cs.LO
Program Equivalence for Algebraic Effects via Modalities
本论文主要研究程序设计语言理论中的程序等价和代数效应。代数效应表示函数式程序设计语言中的不纯行为，如输入和输出、异常、非确定性等，所有这些都以通用的方式处理。程序等价的目的是确定哪些程序在某种意义上可以被认为是等价的。这个问题已经研究了很长时间，但只是最近才扩展到具有代数效果的语言，这是一个较新的发展。为了理解存在代数效应的程序等价性，还有许多工作要做。特别是，没有使用逻辑的上下文对等的特性。我们定义了一个逻辑，其公式表达了高阶程序的代数效果的属性。然后，我们研究了三个概念的程序等价的代数效果：由上述逻辑，应用性双相似性和上下文等价引起的逻辑等价。对于本文所使用的程序设计语言，我们证明了它们都是一致的。因此，本文的主要创新贡献是定义了代数效应的第一逻辑，其诱导程序等价与上下文等价一致。
2019-02-12 cs.LO cs.PL
A Logic for True Concurrency
我们提出了一个逻辑的真正的并发性，其公式谓词的事件在计算和因果关系的依赖关系。诱导的逻辑等价是遗传的历史保持双相似性，和片段的逻辑可以被识别对应于其他真正的并发行为等价在文献中：步骤，pomset和历史保持双相似性。标准的Hennessy-Milner逻辑，因此（交织）双相似性，也被恢复为一个片段。我们还提出了一个扩展的逻辑与不动点算子，从而允许描述因果和并发性质的无限计算。我们相信，这项工作有助于合理介绍真正的并发频谱和更深入地了解所涉及的行为等价物之间的关系。
2014-01-17 cs.LO
Strong Equivalence of Logic Programs with Counting
在答案集编程中，如果两组规则在任何上下文中具有相同的含义，则它们被认为是强等价的。在某些情况下，可以通过从另一个程序的规则中推导出每个程序的规则来建立接地外国佬的输入语言的程序的强等价性。这种证明的可能性已经在该语言的一个子集上得到了证明，该子集包括比较、算术运算和简单的选择规则，但不包括聚合。这个方法在这里被扩展到一类允许使用#count聚合的程序。本文件正在考虑被TPLP接受。
2022-05-16 cs.LO
Automated Verification of Equivalence Properties in Advanced Logic Programs -- Bachelor Thesis
University of Potsdam（波茨坦大学）
本文针对答案集编程在工业应用中的验证需求，扩展工具anthem以支持包含否定、简单选择和池的程序的强等价性验证，提升了关键应用中程序优化的可靠性。
2025-04-14 cs.AI cs.LO
Equivalence Checking By Logic Relaxation
我们介绍了一个新的框架的等价性检查（EC）的布尔电路的基础上的一般技术称为逻辑松弛（LoR）。LoR的本质是放松要求解的公式，并计算新行为集的超集S。也就是说，S包含所有新的满足由于松弛而出现的分配，并且不包含满足原始公式的分配。集合S是由称为部分量词消去的过程生成的。如果所有可能的坏行为都在S中，那么原始公式就不可能有它们，因此这个公式所描述的性质成立。欧共体对《规则》的吸引力是双重的。首先，它有助于生成强大的归纳证明。其次，证明不等价归结为检查放松公式中存在的一些不良行为，即在原始公式的更简单版本中。我们给出了一些实验证据，支持我们的方法。
2016-07-11 cs.LO
Computation Tree Logic with Deadlock Detection
研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。
2009-12-22 cs.LO
On Equivalence of Infinitary Formulas under the Stable Model Semantics
在直觉主义逻辑中等价的命题公式，或者在其扩展中被称为这里和那里的逻辑，具有相同的稳定模型。我们将这个定理扩展到具有无限长合取和析取的命题公式，并展示如何将此推广应用于证明答案集编程中聚合的性质。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-03-26 cs.LO
Equivalence of finite non-deterministic logical matrices is undecidable
本文证明判定两个有限非确定性逻辑矩阵是否等价（诱导相同逻辑）的问题不可判定，并给出了可行的充分条件与特定情形。
2024-12-18 cs.LO math.LO
A Constructive Equivalence between Computation Tree Logic and Failure Trace Testing
形式化验证的两个主要系统是模型检验和基于代数模型的测试。模型检验基于某种形式的时态逻辑，例如线性时态逻辑（LTL）或计算树逻辑（CTL）。CTL是一种强大而现实的逻辑，它能够表达进程的最有趣的属性，如活性和安全性。基于模型的测试基于进程的某些操作语义（例如跟踪、故障或两者）及其关联的前序。除了互模拟之外，最细粒度的前序（主要是理论上的重要性）是基于故障跟踪的。我们表明，这两个最强大的变种是等价的，也就是说，我们表明，对于任何故障跟踪测试存在一个CTL公式相当于它，反之亦然。我们所有的证明都是构造性的和算法性的。我们的结果允许一个大系统的部分被指定为逻辑，而其他部分被指定为代数，从而结合了最好的两个（逻辑和代数）的世界。
2019-01-30 cs.LO
A Logic with Reverse Modalities for History-preserving Bisimulations
我们引入事件标识符逻辑（EIL），它通过增加（1）反向和正向模态以及（2）跟踪事件的标识符来扩展Hennessy-Milner逻辑。我们表明，这种逻辑对应于遗传的历史保持（HH）互模拟等价在一个特定的真并发模型，即稳定的配置结构。此外，我们展示了如何自然子逻辑EIL对应于粗糙的等价。特别地，我们提供了弱历史保持（WH）和历史保持（H）互模拟的逻辑特征。据我们所知，以前已经给出了对应于HH和H互模拟的逻辑，但没有给出对应于WH互模拟的逻辑（当允许自动并发时）。我们还提出了特征公式，它描述了各个结构的历史保存等价。
2011-08-23 cs.LO
A Syntactic Approach to Studying Strongly Equivalent Logic Programs
在应答集程序设计领域中，如果两个逻辑程序在任意扩展下通常等价，则它们是强等价的。这一性质为研究逻辑程序的许多方面提供了理论基础，如程序简化和转换等。因此，ASP及其扩展（如LPMLN）的强等价性得到了广泛的研究。本文提出了一种研究逻辑程序强等价性的句法方法，它提供了一些有趣的结果，有助于我们从一个新的角度理解强等价性。首先，我们提出了独立集的概念和逻辑程序的五种句法变换（S-* 变换）。在ASP和LPMLN的背景下，我们研究了S-* 变换的强等价（SE）和非强等价（NSE）保持性质。其次，基于S-* 变换的性质，我们提出了一个全自动的算法来发现ASP和LPMLN程序保持强等价的语法条件（SE条件）。为了有效地发现SE-条件，我们提出了四种方法来改进算法。第三，我们提出了一个初步的方法来简化已发现的SE-条件，并报告了几种LPMLN程序的简化SE-条件。在此基础上，我们对所发现的SE-条件和存在的问题进行了讨论。最后，我们提出了一个比较SE条件发现方法在本文和相关的工作。
2021-12-06 cs.LO
Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words
University of Warwick（华威大学）
本文提出带作用域的MSO逻辑和数据正则表达式，证明其与NRA在数据域上的等价性，为寄存器自动机提供新的理论基础。
2026-02-13 cs.LO
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
概率自动机已成功地应用于并发和随机系统的形式化验证。有效的模型检验算法已经被研究，其中最常用的用于表达属性的逻辑是基于概率计算树逻辑（PCTL）及其扩展PCTL^*。提出了各种行为等价物，作为一个强大的工具，抽象和组合最小化的PA。不幸的是，这些等价是众所周知的合理的，但就PCTL或PCTL* 所诱导的逻辑等价而言并不完整。塞加拉在1995年指出了一个既健全又完整的行为等价的愿望，但多年来一直没有定论。在本文中，我们引入了新的概念，强互模拟关系，PCTL和PCTL* 的特点。我们扩展了弱互模拟的特点PCTL和PCTL* 没有下一个运营商，分别。此外，我们还扩展了模拟前序的框架。因此，我们的论文弥合了在这种情况下逻辑和行为等价性和前序之间的差距。
2013-06-21 cs.LO
Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
我们研究了在存在副作用的情况下的共代数模态逻辑来验证行为等价性，即，当余代数存在于（余）Kleisli范畴或Eilenberg-Moore范畴中时。我们的目标是开发一个基于索引类别/纤维化的一般框架，这是常见的上述类别。特别是，我们展示了如何从关系提升（一种特殊的索引态射）的行为等价的coalgebraic概念，我们给出了一个一般的配方来构建这样的提升在上述三种情况下。最后，我们应用这个框架来获得（加权）语言等价和条件双相似性的逻辑特征。
2022-02-04 cs.LO
Modal Logic and the Approximation Induction Principle
本文在Hennessy-Milner逻辑的背景下证明了一个紧性定理。它被用来推导出一个充分条件的模态特征的近似归纳原则是健全的模相应的过程等价。我们表明，这个条件是必要的等价问题是合成的投影算子。
2009-11-11 cs.LO
Model-Checking Process Equivalences
过程等价是一种形式化的方法，它将程序和系统联系起来，这些程序和系统在非正式的情况下以相同的方式运行。由于没有唯一的概念，这意味着两个动态系统显示相同的行为有大量的形式过程等价，从互模拟跟踪等价，分类在线性时间分支时间谱。我们提出了一个逻辑框架的基础上表达模态不动点逻辑，它是能够定义许多过程等价关系：对于每个这样的等价有一个固定的公式，这是满足一对过程，当且仅当他们是等价的，就这个关系。我们解释了如何做模型检验，甚至象征性地，这个逻辑的一个重要片段，捕捉许多过程的等价。这允许将模型检验技术用于过程等价性检验。我们展示了如何部分评估可以用来获得决策程序的通用模型检验计划的过程等价。
2012-10-09 cs.LO
Finite Automata Based on Quantum Logic and Their Determinization
给出了正交模格值有限自动机的量子子集构造，并证明了正交模格值有限自动机、正交模格值确定性有限自动机和具有空串移动的正交模格值有限自动机之间的等价性.在此基础上，我们研究了正交模格值正则语言上的代数运算，并在量子逻辑的框架下建立了Kleene定理。
2007-12-28 cs.LO
Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes
本文研究了连续时间马尔可夫决策过程（CTMDPs）的强互模拟等价和弱互模拟等价，以及这些关系在连续时间随机逻辑（CSL）中的逻辑刻画。对于强互模拟，它严格优于CSL等价。本文提出了CTMDPs的强和弱互模拟，并证明了对于CTMDPs的一个子类，强和弱互模拟分别关于CSL和不含next算子的CSL的子逻辑所诱导的等价性都是合理和完备的.然后，我们考虑了CSL的标准扩展，并表明它及其不含X的子逻辑可以分别通过任意CTMDP上的强和弱互模拟来完全表征。
2013-11-16 cs.LO
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
并发系统的基于状态的模型传统上被认为是在各种概念下的进程等价。在标记的过渡系统的特定情况下，这些等价的范围从跟踪等价（强）的双相似性，并组织在什么是所谓的线性时间分支时间谱。通用的共代数和分级单子的组合提供了一个通用的框架，在该框架中，并发的语义可以参数化的分支类型的底层过渡系统和粒度的进程等价。我们表明，在本文件中，这一框架的分级语义subanimate最重要的等价物从线性时间分支时间谱。分级语义的一个重要特征是它允许特征模态逻辑的原则性提取。我们已经建立了这些分级逻辑的不变性下，在早期的工作中给定的分级语义，在本文中，我们扩展了逻辑框架与一个明确的命题层，并提供了一个通用的表达标准，概括了经典的亨尼西-米尔纳定理粗糙的概念过程等价。我们提取分级逻辑的一系列分级语义标记的过渡系统和概率系统，并给出示例性的证明，他们的表现力的基础上，我们的通用标准。
2020-10-20 cs.LO math.CT
Strong Equivalence Made Easy: Nested Expressions and Weight Constraints
逻辑程序P和Q是强等价的，如果给定任何程序R，程序P并集R和程序Q并集R是等价的（即，具有相同的答案集）。强等价性便于研究逻辑程序的等价变换：人们可以证明一个局部变换是正确的，而不需要考虑整个程序。Lifschitz，Pearce和Valverde证明了Heyting的Here-and-There逻辑可以用来刻画带有嵌套表达式的逻辑程序的强等价性（它取代了更著名的扩展析取程序）。本文考虑了这类程序强等价性的一个更简单、更直接的特征，并表明它也可以不加修改地应用于Niemela和Simons的权约束程序。因此，强等价性的这一特征便于研究用回答集程序设计系统dlv和smodels的输入语言编写的逻辑程序的等价变换。该说明的结论是一个简短的讨论的结果，可用于自动推理强等价，包括一种新的编码，减少了问题的决定强等价的一对权重约束程序的决定不一致的权重约束程序。
2003-12-15 cs.AI cs.LO
Quantitative Logics for Equivalence of Effectful Programs
为了对效果进行推理，我们可以定义定量公式来描述有效程序的行为方面。这些公式可以例如表示程序满足属性的概率（或正确的起始状态的集合）。这种方法的基础是定量模态的概念，它用于将值的属性提升为计算的属性。把所有的公式放在一起，我们说两个项是等价的，如果它们在相同的数量程度上满足所有的公式。在数量模态的充分条件下，这种等价性等于阿布拉姆斯基的应用双相似性的概念，而且是一个同余。我们调查这些结果的背景下，利维的呼叫推值一般递归和代数效果。特别是，结果适用于（组合）不确定性的选择，概率的选择，和全球商店。
2019-04-26 cs.LO
Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras
本文研究 Eilenberg-Moore 余代数的分级语义与分级逻辑，证明其能平滑实例化并产生表达性模态逻辑，同时通过量词值单子参数化框架涵盖等价与行为距离。
2024-04-26 cs.LO
Bisimulations and Modal Logics for Higher Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Edinburgh（爱丁堡大学）；University of New South Wales（新南威尔士大学）；University of Warsaw（华沙大学）
该研究针对高维自动机，提出介于ST与hhp互模拟间的新中间等价关系，构建了刻画hhp互模拟的模态逻辑，其片段可刻画ST互模拟及中间概念。
2026-08-17 cs.LO
Interpolant Existence is Undecidable for Two-Variable First-Order Logic with Two Equivalence Relations
本文首次证明一阶逻辑可判定片段中插值存在性问题不可判定，具体包括具有两个等价关系的二变量片段及其有保护扩展，并确定了相应的布尔描述逻辑情形。
2024-04-03 cs.LO math.LO
Simulations and Bisimulations For Coalgebraic Modal Logics
我们定义了一个概念的Lambda模拟的共代数模态逻辑，参数的选择Lambda的谓词提升函子T。我们证明了这个概念在几个方面是足够的：i）它保留了正公式的真值，ii）对于Lambda，单调谓词提升的分离集，Lambda-互模拟的相关概念对应于T-行为等价（此外Lambda-n-互模拟对应于T-n-行为等价），以及iii）事实上，对于Lambda-分离和T保持弱回调，双功能Lambda-互模拟是T-互模拟。从本质上讲，我们得到了一个模块化的等价概念，当与一组单独的单调谓词提升一起使用时，与T-行为等价一致，而不管T是否保留弱回调（与T-双相似性的概念不同）。
2013-04-11 cs.LO math.LO
Weighted Linear Dynamic Logic
本文介绍了一种加权线性动态逻辑（简称加权LDL），并证明了它的公式与加权有理表达式的等价性。这为Schützenberger基本定理增加了一个可识别序列的新特征。令人惊讶的是，等价性不需要对我们的加权LDL进行任何限制。我们的结果保持在任意的（resp。完全完备的半环（分别为）无限）的话。因此，域上加权LDL公式的等价问题在双指数时间内是可判定的。与经典逻辑相比，我们表明，我们的加权LDL是无法表达的加权LTL有限的话。我们确定了一个片段的加权LTL，这样的系列在有限和无限的话定义的LTL公式在这个片段中也可定义的加权LDL公式。
2016-09-14 cs.LO
Limitations of Game Comonads via Homomorphism Indistinguishability
本文通过研究线性代数逻辑中的可逆映射等价（IM），利用同态不可区分性证明了在图范畴上不存在有限秩comonad能刻画IM等价，揭示了博弈comonad方法的局限性。
2023-09-13 cs.LO
Unary negation fragment with equivalence relations has the finite model property
我们考虑一阶逻辑的一元否定片段的扩展，其中任意多个二进制符号可能需要被解释为等价关系。我们证明了这种扩张具有有限模型性质。更具体地说，我们证明了每一个可满足的公式有一个模型，最多双指数大小。我们认为，可满足性（=有限可满足性）的问题，这个逻辑是TwoExpTime完成。我们还将我们的结果转移到一个受限制的变体的守护否定片段的等价关系。
2018-09-13 cs.LO
A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
Chiba University（千叶大学）；Institute of Science Tokyo（东京科学大学）
本文提出了一种扩展的命题动态逻辑，用于描述正则表达式中带lookahead的等价性，并给出了该逻辑的公理化系统，同时证明其计算复杂性与正则表达式相同。
2026-02-10 cs.FL cs.LO
Automated verification of weak equivalence within the SMODELS system
在答案集编程（ASP）中，通过（i）编写其答案集对应于问题的解的逻辑程序，以及通过（ii）使用答案集求解器作为搜索引擎来计算程序的答案集，来解决手头的问题。通常，程序员在优化程序长度和特定求解器上的执行时间时，为特定问题创建一系列逐渐改进的逻辑程序。这将程序员引向确保程序是等效的元级问题，即，它们产生相同的答案集。为了在方法层面简化答案集编程，我们提出了一种基于翻译的方法来验证逻辑程序的等效性。其基本思想是将所考虑的逻辑程序P和Q转换为单个逻辑程序EQT（P，Q），其答案集（如果存在的话）产生P和Q等价的反例。该方法是在这里开发的一个稍微更一般的设置时，考虑到原子的可见性比较答案集。本文提出的基于推理的方法已被实现为一个翻译器，称为lpeq，使验证弱等价的模型系统内使用相同的搜索引擎的搜索模型。我们用lpeq和smodels进行的实验表明，在某些情况下，用这种方式建立逻辑程序的等价性比简单的交叉检查答案集要快得多。
2006-08-25 cs.AI cs.LO
On Uniform Equivalence of Epistemic Logic Programs
University of Klagenfurt（克拉根福大学）；TU Wien（维也纳技术大学）
认知逻辑程序（ELP）扩展了回答集程序设计（ASP）的认知否定，近年来受到了新的关注。这导致了新的研究和有效的解决系统的ELP的发展。在实践中，ELP通常以模块化的方式编写，其中每个模块通过接受事实集作为输入并传递事实集作为输出来与其他模块交互。一个有趣的问题出现了：对于任何输入事实集，在什么条件下这样的模块可以被另一个模块替换而不改变结果？这个问题被称为一致等价，并已被广泛研究的ASP。然而，对于ELP，这种调查迄今为止还没有。因此，在本文中，我们提出了一个表征的一致等价，可以直接应用到语言的国家的最先进的ELP求解器。我们还研究了决定两个ELP一致等价的计算复杂性，并表明它是在多项式层次的第三层。
2019-07-25 cs.AI cs.LO
Pebble games with algebraic rules
我们定义了一个一般框架的分区游戏制定两个球员卵石游戏有限结构。我们表明，一个特定的这样的游戏，我们称之为可逆映射游戏，产生一个家庭的多项式时间近似图同构，严格强于著名的Weisfeiler-Lehman方法。我们介绍的一般框架包括作为特殊情况的卵石游戏有限变量逻辑计数和不计数。它还包括一个矩阵等价游戏，这里介绍，它的特点等价的矩阵秩逻辑的有限变量片段。我们证明了可逆映射游戏定义的等价性是有限变量逻辑中每个游戏定义的等价性的一个改进。
2012-05-07 cs.LO
The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)
我们证明了对于乘法指数线性逻辑（无弱化），割消法所引起的证明的句法等价关系与基于多集的关系模型所引起的证明的语义等价关系一致：一个是说模型（或语义）中的解释是单射的.我们实际上证明了一个更强的结果：两个无割证明的完整的乘法和指数片段的线性逻辑，其解释一致的多集为基础的关系模型是相同的“指数盒的门之间的连接”。
2011-02-07 cs.LO
Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic
本文提出了一种基于线性约束的初等仿射逻辑中的非线性项的类型推断算法。我们证明了算法的正确性和完备性。
2003-05-15 cs.LO
Equivalence of two Fixed-Point Semantics for Definitional Higher-Order Logic Programs
已经提出了两种不同的研究方法分配一个纯粹的扩展语义高阶逻辑编程。前一种方法使用经典的域理论工具，而后者建立在一个固定的点构造上定义的语法实例的源程序。这两种方法之间的关系尚未被调查，直到现在。在本文中，我们证明了对于一类非常广泛的程序，即由W。W. Wadge，这两种方法是一致的（相对于涉及程序符号的基础原子）。另一方面，我们认为，如果存在的高阶变量被允许出现在身体的程序规则，这两种方法是在一般不同的。本文的结果有助于更好地理解高阶逻辑编程的语义。
2015-09-10 cs.LO cs.PL
An introduction to finite automata and their connection to logic
这是一个关于有限自动机的教程。我们提出的标准材料的确定性和最小化，以及一个帐户的等价性有限自动机和一元二阶逻辑。最后，我们介绍了句法幺半群，并作为应用给出了一阶可定义性和非周期性的等价性证明。
2011-09-21 cs.FL cs.LO
Characterising equilibrium logic and nested logic programs: Reductions and complexity
Universidad Politécnica de Madrid（马德里理工大学）；Technische Universität Wien（维也纳技术大学）
平衡逻辑是一种非单调推理的方法，它扩展了逻辑程序的稳定模型和答案集语义。特别是，它包括嵌套逻辑程序的一般情况下，任意布尔组合是允许在头部和身体的规则，作为特殊类型的理论。在本文中，我们提出了多项式减少的主要推理任务与平衡逻辑和嵌套的逻辑程序到量化命题逻辑，扩展经典命题逻辑的原子公式的量化是允许的。我们不仅为决策问题提供约简，而且为平衡逻辑和嵌套逻辑程序的中心语义概念提供约简。特别是，我们的编码映射一个给定的决策问题到一些公式，后者是有效的，正是在前者举行。我们在这里处理的基本任务是一致性问题，勇敢推理和怀疑推理。此外，我们还提供了编码测试等价的理论或程序下的不同概念的等价性，即普通，强，一致等价。对于所有考虑的推理任务，我们分析了它们的计算复杂性，并给出了严格的复杂性界限。
2009-06-13 cs.AI cs.LO
Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking
The Chinese University of Hong Kong（香港中文大学）；National Center of Technology Innovation for EDA（EDA技术国家创新中心）；Southeast University（东南大学）
研究逻辑等效性检查中因结构扰动等导致的问题，提出斜接感知映射框架，集成等效保留映射、高斯引导异或建模和面向求解器的查找表选择三种技术，可提升LEC效率，在数据集上有显著效果。
2026-07-09 cs.AR cs.LO
Hennessy-Milner Theorems via Galois Connections
我们介绍了一个一般的和成分，但简单的框架，使我们能够得到健全性和表现力的结果，模态逻辑特征的行为等价性或度量（也被称为亨尼西-米尔纳定理）。它是基于伽罗瓦连接集（实值）谓词的一方面和等价关系/度量的另一方面，并涵盖了一部分的线性时间分支时间谱，无论是定性的情况下（行为等价）和定量的情况下（行为度量）。我们从一个给定的逻辑推导出行为函数，并给出一个条件，称为兼容性，其特征在于在哪些条件下逻辑诱导的等价性/度量是由不动点方程诱导的。特别是这个框架，使我们能够得到一个新的定点表征定向跟踪度量。
2023-01-14 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
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
循环证明系统为我们提供了另一种表示归纳定义和有效证明搜索的方法。2011年，Brotherston和Simpson证明了经典循环证明系统的可证明性与马丁-洛夫归纳定义的经典系统的可证明性之间的等价性。本文研究直觉逻辑中的猜想。本文首先指出，FOSSACS 2017年论文的反模型表明直觉逻辑的猜想一般是错误的。然后证明了直觉逻辑的猜想在算术下成立，即直觉循环证明系统与Martin-Lof归纳定义的直觉系统在都包含Heyting算术HA时的可证性相同。为此，本文还证明了HA证明了归纳法的Podelski-Rybalchenko定理和归纳法的Kleene-Brouwer定理。这些结果立即为同一作者在LICS 2017论文中提出的经典逻辑算术下的猜想提供了另一个证明。
2017-12-10 cs.LO math.LO
Using Modes to Ensure Subject Reduction for Typed Logic Programs with Subtyping
我们考虑了逻辑程序的一个具有参数多态性和子类型的一般规定类型系统。主语归约的性质表达了类型系统相对于主系统的一致性。执行模型：如果一个程序是“良好类型的”，那么所有从“良好类型的”目标开始的派生都是“良好类型的”。众所周知，对于逻辑程序，如果没有子类型，这个性质很容易获得。他们的标准（非类型化）执行模型。在这里，我们给出的句法条件，确保主题减少，也在一般的子类型之间的关系类型构造。其思想是考虑具有由模式给出的固定的逻辑流的逻辑程序。
2001-01-18 cs.LO
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.LO
