Modal Logics for Nominal Transition Systems
本文为名义转换系统定义了通用模型及Hennessy-Milner逻辑，证明其充分且表达完备，并系统处理多种互模拟变体，已在Nominal Isabelle中形式化。
2021-01-27 cs.LO
Nominal Logic Programming
名义逻辑是一阶逻辑的扩展，它为抽象语法的形式化和推理提供了一个简单的基础，模一致的重命名的绑定名称（即α-等价）。本文研究基于名义逻辑的逻辑程序设计。我们描述了一些典型的名义逻辑程序，并发展了这类程序的模型论、证明论和操作语义。除了确保实现的正确行为的兴趣，这些结果提供了一个严格的基础技术分析和推理的名义逻辑程序，我们通过例子说明。
2007-08-20 cs.LO cs.PL
Formalising the pi-calculus using nominal logic
我们使用名义数据类型包形式化pi演算，基于Pitts等人的名义逻辑思想，并演示了在Isabelle/HOL中的实现。其目的是为了进行机器可检查的证明，严格遵循在手动证明中发现的直观参数，推导出强大的归纳规则的语义。通过这种方式，我们已经涵盖了互模拟等价和同余的许多标准定理，无论是早期的还是晚期的，无论是强的还是弱的。因此，我们提供了一个最广泛的形式化的过程演算内做过的定理证明。在我们的配方中的一个显着的收获是，代理商被确定为α-等价，从而大大减少了绑定名称的参数。这是一个关于π演算的手动证明的正常策略，但这种挥手以前很难顺利地纳入交互式定理证明器。我们展示了如何名义逻辑形式主义和它的支持伊莎贝尔完成这一点，从而显着减少了繁琐的进行完全正式的证明。这改进了以前使用弱高阶抽象语法的工作，因为我们不需要额外的假设来过滤掉外来项，并且可以将所有参数保持在熟悉的一阶逻辑中。
2009-06-30 cs.LO
Psi-calculi: a framework for mobile processes with nominal data and logic
psi演算的框架扩展了pi演算的数据结构和逻辑断言和条件的名义数据表。它们可以在进程之间传输，并且它们的名称可以像标准pi演算中那样静态地作用域。Psi演算可以捕获与其他提出的pi演算扩展相同的现象，例如应用pi演算，spi演算，融合演算，并发约束pi演算，以及具有多元通信信道或模式匹配的演算。PSI演算甚至可以更通用，例如允许结构化通道，高阶形式主义，如用于数据结构的λ演算，以及用于断言的谓词逻辑。我们提供了充分的比较，相关的结石，并讨论了一些重要的应用。我们标记的操作语义和互模拟的定义是直接的，没有结构一致性。我们建立最低要求的名义数据和逻辑，以证明一般代数性质的PSI演算，所有这些都已检查的互动定理证明伊莎贝尔。PSI演算的表达性明显超过其他形式主义，而语义的纯度与原始的PI演算相当。
2011-03-31 cs.LO
Nominal Abstraction
递归关系规范通常用于描述形式系统的计算结构。最近的研究证明理论已经确定了两个功能，促进直接的，基于逻辑的推理这样的描述：通过递归定义的原子判断的解释和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑目前不允许定义体现与绑定相关的动态方面的关系，这是许多推理任务所需的能力。我们提出了一个新的术语之间的关系称为名义抽象作为克服这一缺陷的一种手段。我们将名义抽象到一个丰富的逻辑，也包括定义，通用量化，归纳，并共同归纳，然后我们证明是一致的。我们提出的例子表明，这种逻辑可以提供优雅的治疗绑定的情况下，出现在许多证明，如那些建立属性的类型演算和任意级联替代，在reductionalarguments中发挥作用。
2010-09-23 cs.LO
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
本文探讨了必要的证明理论推荐一个富有表现力的，但可判定的一阶系统，名为MAV 1，具有德摩根对偶对名义量词。这些名量词被称为“新”和“文”，不同于自对偶的Gabbay-Pitts和Miller-Tiu名量词。这些名词性量词的新颖之处在于它们是两极分化的，在这个意义上，“新”分布在积极的运营商，而“文”分布在消极的运营商。这种对簿记的更大控制使私有名称能够在MAV 1中嵌入公式的过程中建模。技术上的挑战是建立一个割消结果，从其中的基本性质，包括传递性的蕴涵遵循。由于该系统是使用微积分的结构，一个概括的微积分，新的技术被采用。证明依赖于一个复杂设计的基于多集的证明大小的度量，它被用来指导一种称为分裂的规范化技术。在分裂证明中，交换连续量词的等方差的存在导致了名义量词、加法合取算子和乘法算子之间复杂的相互依赖。每一条规则都通过一个例子来证明，为什么这条规则对于合理地嵌入流程和确保削减消除是必要的。
2020-01-15 cs.LO
Consequence-based Reasoning for Description Logics with Disjunction, Inverse Roles, Number Restrictions, and Nominals
University of Oxford（牛津大学）
我们提出了一个基于结果的演算的概念包容和分类的描述逻辑ALCHOIQ，它扩展了ALC的角色层次结构，逆角色，数量限制，和名词。通过使用标准的转换，我们的演算扩展到SROIQ，它涵盖了所有的OWL 2 DL除了数据库。我们的演算的一个关键特征是它的现收现付行为：与现有的算法不同，我们的演算对于所有已知的ALCHOIQ适当片段都是最坏情况下的最优，尽管不是对于完整的逻辑。
2018-05-03 cs.AI cs.LO
Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits
本文提出一种谓词逻辑模型，其中每个术语和谓词都有独立于变量赋值的绝对指称，通过代数和替换、量词等概念实现，并证明了普通模型可转换为该模型，从而证明了完备性。
2023-12-27 cs.LO
Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
通过对模型的操作，我们展示了如何将允许标称模型的完备性与有限支持的标称模型的完备性联系起来。有限支集模型是容许名义模型的一种特殊情况，因此构造取决于从后者的一个实例生成前者的某个实例，其中元素之间保留了足够多的不等式。我们这样做使用一个无限的广义的名义原子抽象。结果本身就很有趣，但我们也考虑了数学因素，以便最大限度地提高它也可以用于其他名义推理系统的机会。具有无限支撑的模型可以更容易地工作，因此有一个半自动定理将结果从无限支撑的名义模型类转移到具有有限支撑的更具限制性的模型类是有用的。最后，我们考虑不同的允许名义语法和名义模型，并讨论它们如何与这里证明的结果。
2011-12-05 cs.LO math.LO
Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
本文针对含名词和角色包含的描述/模态逻辑不具备CIP与PBDP的问题，证明插值元与显式定义存在性仍可判定，明确不同场景下的复杂度，并给出适用于含角色包含描述逻辑的计算算法。
2023-04-28 cs.LO
Nominal Matching Logic
我们引入名义匹配逻辑（NML）作为匹配逻辑的扩展与名称和绑定以下的Gabbay-Pitts名义的方法。匹配逻辑是$\mathbb{K}$框架的基础，用于指定程序设计语言并自动派生相关工具（编译器、调试器、模型检查器、程序验证器）。匹配逻辑不包括名称绑定的原始概念，尽管绑定运算符可以通过编码来表示，该编码将函数的图从绑定名称内部化为包含绑定名称的表达式。这种方法足以表示涉及绑定运算符的计算，但是还没有与对具有绑定的语法的归纳推理的支持相协调（例如，对$λ$项的推理）。名词逻辑是一个关于名称和绑定的形式化推理系统，它为基于绑定的语法的归纳推理提供了良好的和强大的原则，NML继承了这些原则。我们讨论了NML的语法和语义的设计方案，证明元理论的属性，并给出例子来说明其表达能力。特别是，我们展示了如何归纳原则$λ$ -条款（$α$ -结构归纳）可以定义和用于证明标准属性的$λ$ -演算。
2022-07-28 cs.LO cs.PL
A Nominal Approach to Probabilistic Separation Logic
本文通过建立概率分离逻辑中基于测度论的分解与概率空间中基于乘积的分解之间的范畴等价，弥合了概率论与概率程序形式化推理之间的差距，并验证了先前设计决策。
2024-05-29 cs.LO cs.PL
Nominal Unification from a Higher-Order Perspective
名义逻辑是一阶逻辑的一个版本，具有相等性，名称绑定，通过名称交换重命名和名称的新鲜性。类似于高阶逻辑，可绑定的名称，称为原子，和可实例化的变量被认为是不同的实体。此外，原子可以通过实例化来捕获，这打破了原子演算的基本原则。尽管有这些差异，名义统一可以从更高层次的角度来看。从这个角度来看，我们表明，名义统一可以减少到一个特定的片段高阶统一问题：高阶模式统一。这种减少证明，名义统一可以决定在二次确定性时间，使用高阶模式统一的线性算法。我们还证明了翻译保持最一般的统一。
2010-05-20 cs.LO cs.SC
Toward Structured Proofs for Dynamic Logics
我们提出Kaisar，差分动态逻辑（dL）的结构化交互式证明语言，安全关键的网络物理系统（CPS）。Kaisar的定义特征是 *nominal terms*，它通过将经常需要的对过去程序状态的历史引用作为一流的来简化CPS证明。为了支持名词，我们扩展了结构化证明的概念，并将CPS模型的 * 结构化符号执行 * 作为一级概念。我们实现Kaisar在定理证明器KeYmaera X和再现降落伞的安全操作和地面机器人控制的案例研究的一个例子。我们展示了如何名词简化常见的CPS推理任务时，结合其他功能的结构化证明。我们为凯撒开发了一个广泛的元理论。除了健全性和完整性，我们显示了一个正式的规范Kaisar的名词，并与Kaisar的名义上的dL的变体。
2019-08-15 cs.LO cs.PL
Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Oxford University Computing Laboratory（牛津大学计算实验室）
描述逻辑是知识表示的形式主义，它提供了例如W3C OWL标准的逻辑基础。合取查询是数据库中的标准查询语言，作为查询描述逻辑知识库的一种表达形式，近年来得到了广泛的关注。几种不同的技术，决定合取查询蕴涵可用于广泛的DL。然而，OWL 1和OWL 2 DL中的名词、逆角色和数量限制的组合导致了迄今为止可用的技术无法解决的问题。我们解决这个问题，并提出了一个决定性的结果蕴涵工会的合取查询在DL ALCHOIQb，同时包含所有三个有问题的建设者。提供查询只包含简单的角色，我们的结果也显示了可判定性蕴涵（工会）合取查询的逻辑，支持OWL 1 DL，我们相信，所提出的结果将铺平道路，进一步取得进展合取查询蕴涵决策程序的描述逻辑基础的OWL标准。
2014-01-16 cs.AI cs.LO
Closed nominal rewriting and efficiently computable nominal algebra equality
本文分析了名义代数与名义重写的关系，给出了名义理论中方程演绎的一种新的简明表述。我们利用一些新的结果，证明了一个方程理论的子类，其中名义重写提供了一个检查名义代数等式的完整过程。这个子类包含了微积分和一阶逻辑的规范。
2010-09-14 cs.LO cs.PL
Semantics out of context: nominal absolute denotations for first-order logic and computation
Heriot-Watt University（赫瑞-瓦特大学）
本文提出三种绝对语义方法，通过 lattice、集合和代数结构处理一阶逻辑中的变量，引入'fresh-finite'极限和新型替代 dual，为逻辑与计算基础提供新视角。
2016-01-05 cs.LO math.LO
Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders
针对带绑定符、新鲜性条件和等式公理的场景下等式推理难题，提出模等式理论的nominal重写与窄化框架，证明关键性质与提升定理，开发出正确的nominal合一过程并通过示例验证有效性。
2025-05-20 cs.LO
Introducing Nominals to the Combined Query Answering Approaches for EL
University of Oxford（牛津大学）
所谓的组合方法在三个步骤中回答描述逻辑本体上的合取查询：首先，它们具体化本体和数据的某些结果;第二，它们评估数据上的查询;第三，它们过滤第二阶段的结果以消除不合理的答案。这种方法是为DL-Lite和EL语言家族的各种成员开发的，但它们都不能处理包含名词的本体。在我们的工作中，我们弥合了这一差距，并提出了一个组合的查询回答方法ELHO-一个逻辑，包含所有功能的OWL 2 EL标准除了传递角色和复杂的角色夹杂物。这个扩展是不平凡的，因为名词需要等式推理，这将复杂性引入了第一步和第三步。我们的实证评估表明，我们的技术是适合于实际应用，因此它提供了一个实际的基础上，在一个大片段的OWL 2 EL的合取查询回答。
2013-04-01 cs.AI cs.DB cs.LO
Nominal Equational Rewriting and Narrowing
本文首次定义等式理论取模下的标称重写与窄化，建立标称E-一致性并证明标称E-提升定理，为通过标称等式窄化实现正确的标称等式合一算法奠定理论基础。
2025-06-06 cs.LO cs.SC
Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
Otto-Friedrich-Universität Bamberg（班贝格奥托-弗里德里希大学）；Freie Universität Berlin（柏林自由大学）
本文通过机械分析浅嵌入证明，证实哥德尔本体论论证的294个定理均可在无名义词的对象语言内证明，并修正合取公理后解决了《数学月刊》笔记遗留的三个开放问题。
2026-11-03 cs.AI cs.LO math.LO
Strong Nominal Semantics for Fixed-Point Constraints
本文扩展名义代数引入固定点约束，用强名义集合提供可靠语义，并针对名义集合不可靠问题提出两种恢复可靠性的公式化方法。
2024-12-07 cs.LO
Equational Reasoning Modulo Commutativity in Languages with Binders (Extended Version)
本文在 nominal 语言中引入基于置换不动点约束的 nominal 代数，将交换性无缝集成到 $α$-等价推理中，提出并证明终止且正确的模交换性 nominal 合一算法，为带绑定符和交换算子的语法结构归纳与递归提供可靠基础。
2025-03-01 cs.LO
Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$
Catskills Research Company（卡茨基尔研究公司）
本文在 Lean 4 中完成了混合逻辑 $L(\forall)$ 的机器检查完备性证明，通过结构新鲜性和存在引理 Henkin 构造两种工具解决了新鲜名称的生成问题。
2026-06-19 cs.LO math.LO
Logic Column 12: Logical Verification and Equational Verification
本文研究了两种验证方法，一种是基于使用逻辑来表达系统的属性，另一种是基于将系统等效于一个简单的系统，该系统显然具有感兴趣的任何属性。使用的例子，如过程演算和常规程序，这两种方法之间的关系进行了探讨。
2005-05-10 cs.LO
Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
本文研究逻辑约束项重写的语义，定义受约束等式、等式理论及有效性，构建可靠推理系统并提出代数语义以判定无效性和新的一致性概念。
2024-07-05 cs.LO
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
我们提出了一个共归纳的框架，定义和推理的无穷类似物的方程逻辑和长期重写在一个统一的，共归纳的方式。该设置捕获任意序数长度的重写序列，但它既不需要序数也不需要度量收敛。这使得该框架特别适合于定理证明器中的形式化。
2018-01-09 cs.LO
String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS (Full Version)
我们研究了以连接和有限状态转换器作为原子操作的弦逻辑的可满足性的判定性的基本问题。虽然限制到一种类型的操作产生的可判定性，很少有人知道他们的组合理论，这是特别相关的动态网页在一个更现实的浏览器模型的安全漏洞分析时的可判定性。一方面，单词方程（带有连接的字符串逻辑）不能精确地捕获清理功能（例如htmlescape）和隐式浏览器转换（例如innerHTML突变）。另一方面，转换器遭受能够对消毒功能和浏览器转换建模，但不能对字符串连接建模的相反问题。简单地将词方程和转换器组合在一起很容易导致不可判定的逻辑。我们的主要贡献是表明，“直线片段”的逻辑是可判定的（复杂性范围从PSPACE到EXPSPACE）。该片段可以表达的程序逻辑的直线字符串操作程序的连接和转换作为原子操作，这出现在执行有界模型检验或动态符号执行。我们证明了逻辑可以自然地表达分析Web应用程序中的突变XSS所需的约束。最后，在存在长度、字母计数、正则、indexOf和不等性约束的情况下，逻辑仍然是可判定的。
2015-11-05 cs.LO
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
在这项工作中，我们考虑的可满足性问题的逻辑，结合字方程的字符串变量表示的话的无限长度，正则语言的话属于Presburger限制的话的长度。我们提出了一种新的决策过程，在两个可决策的片段，包括二次字方程（即，每个字符串变量最多出现两次）。所提出的过程减少了问题解决的Presburger算法的可满足性。该过程结合了两个主要组成部分：（i）一个算法，以获得一个完整的一组所有的解决方案的词方程和正则表达式的连接;和（ii）两种方法，以精确计算关系约束的字符串长度所隐含的所有solutions.We已经实现了一个原型工具，并评估了一组可满足性问题的逻辑。实验结果表明，该工具是有效和高效的。
2018-05-23 cs.LO
Recording Completion for Finding and Certifying Proofs in Equational Logic
当我们想回答/证明一个给定的方程是否由一个方程系统所蕴涵时，我们面临以下问题：（1）很难找到一个转换（但很容易证明一个给定的转换）。(2)在Knuth-Benzen完备化成功的假设下，判定转换的存在是容易的，但很难证明这一判定。在本文中，我们介绍记录完成，它克服了这两个问题。
2012-08-08 cs.LO
Fixed-Points for Quantitative Equational Logics
我们发展了定量方程逻辑的一个不动点扩展，并给出了有界完备定量代数的语义。与以前关于度量空间中不动点的相关工作不同，我们使用近似相等而不是精确相等的概念。其结果是一个新的理论的不动点，它不仅可以提供解决传统的不动点方程，但我们也可以定义收敛到不动点的速度。我们表明，这样一个理论是定量模拟的康威理论，也是迭代理论，它反映了度量coinduction原则。我们研究了Bellman方程的马尔可夫决策过程作为一个说明性的例子。
2021-06-30 cs.LO
A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）
本文提出实解析微分代数动态逻辑的证明演算，用于正确转换微分代数方程，实现微分代数方程到常微分方程的降阶，并确保与混合系统中的微分形式动态逻辑兼容。主要贡献是鬼切换，用于将多模系统分解为混合系统，正确混合复杂的微分代数动力学。
2025-05-25 cs.LO
Infinitary Classical Logic: Recursive Equations and Interactive Semantics
在本文中，我们提出了一个经典逻辑的无限扩展派生的交互语义。我们语言的公式可能是由命题变量和逻辑连接词标记的无限树。我们表明，在我们的设置每个递归公式方程有一个唯一的解决方案。至于导子，我们使用Tait演算的无穷变体来导出序列。我们在本文中介绍的派生的交互式语义被表示为测试<< T >>（派生候选者，Proponent）和环境<< not S >>（否定对象，Opponent）之间的辩论（交互树）。我们证明了一个推导的完备性定理，我们称之为交互完备性定理：<< T >>（测试）和<< not S >>（环境）之间的交互不会产生错误（即，Proponent wins）以防<< T >>来自< >的句法派生< S >。
2014-09-11 cs.LO
Controlling program extraction in Elementary Linear Logic
本文提出了一种基于初等线性逻辑中程序抽取的Krivine & Leivant系统FA_2的自适应方法。该系统允许编写高阶方程，以指定提取程序的计算内容。然后，用户可以证明一个通用公式，使用这些方程作为公理，其证明可以提取到程序中，在基本时间规范化并满足规范。最后，我们证明了所有的初等递归函数都可以在这个系统中实现。
2010-06-14 cs.LO
Untyping Typed Algebras and Colouring Cyclic Linear Logic
我们证明了“untyping”定理：在一些类型理论（半环，Kleene代数，剩余格，对合剩余格），类型方程可以从底层untyped方程。因此，相应的非类型化决策过程可以免费扩展到类型化设置。其中一些定理是通过迂回循环线性逻辑的片段获得的，并对标准证明搜索算法进行了大量优化。
2012-06-19 cs.LO
Non-commutative propositional logic with short-circuited biconditional and NAND
短路求值（Short-circuit evaluation）表示命题连接词的语义，其中只有当第一个参数不足以确定表达式的值时，才对第二个参数求值。在程序设计中，短路求值被广泛使用，左序合取和析取作为原始连接词。我们考虑左序，非交换命题逻辑，也被称为MSCL（记忆短路逻辑），并从以前出版的，等式公理化。首先，我们扩展这个逻辑的左序版本的双连续连接，这使得一个优雅的axiomatisation的MSCL。接下来，我们考虑一个左顺序版本的NAND操作（谢弗中风），并再次给出一个完整的，等式axiomatisation相应的变体MSCL。最后，我们认为这些逻辑系统中的一个三值设置为“未定义”的常数，并再次提供完整性的结果。
2022-03-17 cs.LO
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
本文研究图上概率编程语言的语义模型，建立其与图子的联系，证明良态等式理论与图子一一对应，并通过Markov范畴、测度论概率和名义集合三种构造证明所有图子均源于等式理论，从而构建了图概率编程新模型。
2023-12-28 cs.LO cs.PL math.PR
On the mathematical synthesis of equational logics
我们提供了一个数学理论和方法，从代数元理论合成方程逻辑。我们说明了我们的方法，通过两个应用程序：一个合理的重建Birkhoff的方程逻辑和一个新的方程逻辑推理代数结构与名称绑定运营商。
2011-09-07 cs.LO math.CT math.LO
A first-order logic for string diagrams
用弦图进行方程推理提供了一种直观的方法来证明对称幺半范畴中态射之间的方程。这可以扩展到使用一个简单的图形语法来证明无限族的方程，称为！-方框符号虽然这确实大大增加了字符串图的证明能力，但以前超越等式推理的尝试在很大程度上是临时的，因为缺乏合适的逻辑框架来进行涉及！箱.在本文中，我们将等式推理扩展为！框到一个完全成熟的一阶逻辑，称为连接，含义和全称量化！-箱.这个逻辑，叫做！L，则足够丰富以适当地形式化归纳原理，箱.然后我们建立一个标准模型！并给出一个非交换双代数的定理的例子证明！L，这是无法通过等式推理单独获得的。
2015-05-02 cs.LO math.CT
Static Analysis Techniques for Equational Logic Programming
等式逻辑程序是一组有向等式或规则，用于以明显的方式进行计算（通过用"更简单“的等式替换等式）。我们提出了静态分析技术，有效的方程逻辑编程，其中一些已实施的$LR^2$，实验室开发和评估快速，高效，实用的重写技术。$LR^2$的两个新特性是在大多数情况下允许非左线性规则，并且它具有基于同余闭包算法的制表选项来计算范式。虽然，本研究的重点是在表的方法，一些技术也适用于非表的方法。我们的演示是在$LR^2$的上下文中进行的，它是一个解释器，但其中的一些技术也适用于编译。
2000-10-27 cs.LO cs.PL
Existentially Quantified Systems of Equations as an Implicit Representation of Answers in Logic Programming
在本文中，我们提出了另一种方法来形式化的逻辑编程理论。在这种形式化中，我们允许在查询中存在量化变量和方程。与标准方法相反，答案的作用将由存在量化的方程组发挥。这使得我们在处理替换时可以避免问题。特别地，当输入子句引入新变量时，我们不需要“全局”变量分隔条件。此外，这种形式化可以被视为并发逻辑语言理论的基础，因为它还包括广泛的并行计算方法。此外，答案的平行组合可以直接定义为答案的一致连接。
2022-07-19 cs.LO cs.PL
Definability of linear equation systems over groups and rings
出于对PTIME逻辑的追求和最近的见解，从线性代数问题的描述复杂性是这个问题的一个重要方面，我们研究了线性方程组的可解性有限群和环的逻辑（间）定义的观点。我们考虑的所有问题都是在多项式时间内可判定的，但不能用带计数的不动点逻辑来表示。他们还提供了一个自然的候选人分离的多项式时间从秩逻辑，扩展不动点逻辑的运营商确定的秩可定义的矩阵，这是足够的可解性问题领域。基于有限环的结构理论，我们建立了各种可解性问题的逻辑归约。我们的研究结果表明，所有的线性方程组的可解性问题，分离不动点逻辑计数PTIME可以减少到可解性交换环。此外，我们证明了封闭性质的查询类，减少到可解性环，这提供了范式的逻辑扩展与可解性运营商。我们的结论是研究在何种程度上的不动点逻辑计数可以表示问题的线性代数有限交换环，推广已知的结果在有限域的线性代数问题的逻辑定义。
2013-11-11 cs.CC cs.LO
A Decision Procedure for String Logic with Equations, Regular Membership and Length Constraints
本文研究了长度函数上具有方程、正则隶属和Presburger约束的串逻辑的可满足性问题。困难来自于字符串变量的多次出现，使得最先进的算法无法终止。我们的主要贡献是表明，可满足性问题的片段中没有字符串变量出现两次以上的方程是可判定的。特别是，我们提出了一个半决策过程的任意字符串公式与字方程，经常成员和长度功能。我们的过程的本质是一个算法，枚举一个等价的一组可解析取公式。我们进一步表明，该算法总是终止上述可判定的片段。最后，我们提供了我们的决策过程的复杂性分析，以证明它运行，在最坏的情况下，在阶乘时间。
2016-10-11 cs.LO cs.PL
An abstract fixed-point theorem for Horn formula equations
TU Wien（维也纳工业大学）；University of Amsterdam（阿姆斯特丹大学）
针对计算机科学多应用中重要的Horn公式方程，本文在带最小不动点算子的一阶逻辑中证明了适用于抽象语义的抽象不动点定理，并阐述其在程序验证逻辑基础等计算逻辑领域的推论。
2025-11-11 cs.LO math.LO
On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
本文针对命题动态逻辑中的不动点方程，提出由两个对偶层级构成的新公式类，证明其方程必有解，并给出每个方程的显式解。
2024-12-05 cs.LO math.LO
Resolving Gödel's Incompleteness Myth: Polynomial Equations and Dynamical Systems for Algebraic Logic
本文介绍了一种新的计算方法，即利用多项式方程和动力系统来计算逻辑命题，并将其应用于哥德尔不完备性定理。逻辑公式服从一组公理的真假值是从相应的多项式方程系统的解计算出来的。一个公式引用其自身的可证明性被证明是一个递归关系，它可以被解释为这样产生一个离散的动力系统，或解释在一个静态的方式来创建一个额外的联立方程。在这个框架中，逻辑公式和其他多项式目标的真假值具有复杂的数据结构：基本值的集合，或者生成这种解值集合的无穷序列的动力系统。除了公式具有确定的基本值这一常规结果外，这些数据结构还编码了几种例外情况：模糊的、不可满足的、不稳定的或偶然的公式。这些例外代表了几种语义上不同类型的不可判定性;没有一个会给数学带来任何基本问题。很容易计算出哥德尔公式，它断言它不能被证明，在特定的方面是例外的：静态地解释，公式定义了一个矛盾方程组（因此它被称为不可满足的）;动态地解释，它定义了一个动力系统，有一个周期轨道，没有不动点（因此它被称为不稳定的）。这些例外并不是逻辑上的灾难性失败;它们是对哥德尔自指结构的精确数学描述。哥德尔的分析并没有揭示任何实质性的不完整性，在正式的推理系统，也没有任何障碍，证明这种系统的一致性，由普通的数学手段。
2011-12-21 cs.LO math.GM
Monadic second order logic as the model companion of temporal logic
本文的主要重点是互模拟不变的MSO，更具体地说，在模型论中，一个理论的模型伴侣是一类模型的一阶描述，其中所有潜在的可解方程组和非方程组有解决方案。我们发现，双模拟不变的MSO树模型伴侣的一个新的时态逻辑，“公平CTL”，丰富的CTL与当地的公平性约束。为了实现这一点，我们给出了一个完整的证明，逻辑公平CTL相结合的tableaux和石头对偶，和一个公平的CTL编码的自动机的模态μ演算。此外，我们还证明了二叉树上的MSO是二元确定性公平CTL的模型伴侣。
2016-05-03 cs.LO math.LO
