Aperiodic Weighted Automata and Weighted First-Order Logic
根据Schützenberger，McNaughton和Papert在1970年代的基本结果，一阶可定义语言和非周期语言的类别是一致的。在这里，我们将这种等价性扩展到定量设置。为此，加权自动机形成了一个通用的和广泛研究的模型。我们定义了一个合适的加权一阶逻辑的概念。然后，我们证明了这种加权一阶逻辑和非周期多项式模糊加权自动机具有相同的表达能力。此外，我们还得到了适当的加权子逻辑和无二义性或无二义性的非周期加权自动机的等价结果。我们的结果适用于一般的重量结构，包括所有半环，平均计算的成本，有界格，和其他。
2019-09-30 cs.FL cs.LO
Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics
我们引入了分支传递闭包算子的加权一元二阶逻辑公式的分支对应于一个自然的方式在树中固有的分支。对任意交换半环，我们证明了树上的加权一元二阶逻辑等价于由下列算子之一开始的公式的可定义性：（i）分支传递闭包或（ii）存在二阶量词后接泛一阶量词;在这两种情况下，该运算符被应用于（a）通过模计数而丰富的布尔一阶逻辑或（b）布尔一元二阶逻辑上的步进公式。
2015-04-29 cs.FL cs.LO
Multi-weighted Automata and MSO Logic
加权自动机是一种非确定性自动机，其中的转换都带有权值。它们可以模拟系统的定量方面，如成本或能耗。运行的值可以被计算为例如转变权重的最大值、极限平均值或折扣总和。在多重加权自动机中，转换带有多个权重，并且可以模拟例如奖励和成本之间的比率，或者在二级资源上的某个上限约束下的主要资源的使用效率。在这里，我们介绍了一个一般模型的多加权自动机以及多加权MSO逻辑。在我们的主要结果中，我们表明，这种多加权MSO逻辑和多加权自动机是表示等价的有限和无限的话。翻译过程是有效的，导致我们的多加权MSO逻辑的可判定性结果。
2015-06-19 cs.FL cs.LO
Weighted Automata and Logics for Infinite Nested Words
Nested words由Alfred和Madhusudan引入，用于捕获具有线性和层次顺序的结构，例如XML文档，而不会丢失有价值的闭包属性。此外，Büchi和Madhusudan为有限和无限嵌套词引入了自动机和等价逻辑，从而将Büchi定理扩展到嵌套词。最近，在定量系统中的权重的平均和折扣计算发现了很大的兴趣。在这里，我们将介绍和研究加权自动机模型和加权MSO逻辑无限嵌套的话。作为权重结构，我们考虑赋值幺半群，它包含权重的平均和折扣计算以及经典的半环。我们表明，在适当的假设下，两个分别。我们的加权逻辑的三个片段可以相互转换。此外，我们表明，逻辑片段具有相同的表达能力加权嵌套词自动机。
2015-06-23 cs.FL cs.LO
On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
University of Bologna, Italy（博洛尼亚大学）；INRIA Sophia Antipolis, France（法国索菲亚安提佩利斯国家信息与自动化研究所）；Université Claude Bernard Lyon 1, France（法国里昂第一大学）
本文研究了概率高阶递归方案的终止问题，利用线性逻辑的加权关系语义将问题转化为生成函数的计算，证明了在扩展Li等人affine PHORS的类型纪律下，几乎必然终止的可判定性。
2026-04-30 cs.LO
Tensors over Semirings for Latent-Variable Weighted Logic Programs
University of Edinburgh（爱丁堡大学）；University of Rochester（罗切斯特大学）
半环分析是一个优雅的框架，通过使用半环加权逻辑程序来描述分析器。在本文中，我们提出了这个概念的推广：潜变量半环分析。与我们的框架，任何半环加权逻辑程序可以通过转换权重从半环的标量值的秩n数组，或张量，半环值，允许半环解析框架内的潜在变量的建模。在处理张量时，半环是一个太强的概念，我们不得不求助于一个较弱的结构：部分半环。我们证明，这种推广保留了所有所需的原始半环框架的性质，同时严格增加其表现力。
2020-06-07 cs.CL cs.LO
Modelling architectures of parametric weighted component-based systems
复杂软件系统的设计通常是由多个协调的组件和未知数量的实例组成的。对于这样的系统，一个主要的挑战是有效地建模其架构，确定拓扑结构和组件之间的交互原则。为了实现良好的设计，需要解决软件架构的定量方面。在本文中，我们研究的建模问题的软件体系结构的参数加权组件为基础的系统中的参数是每个组件的实例的数量。为此，我们引入了一个加权的一阶扩展的交互逻辑交换半环，以作为参数量化架构的建模语言。证明了该逻辑公式的等价问题在体类（子半环类）中是可判定的。此外，我们表明，我们的加权逻辑可以有效地描述众所周知的参数结构的定量特征。
2020-04-26 cs.LO
Weighted Automata and Monadic Second Order Logic
设S是交换半环。M. Droste和P.Gastin在2005年引入了加权一元二阶逻辑WMSOL，其权在S。他们使用WMSOL的语法片段RMSOL来表征加权自动机可识别的词函数（幂级数），其中量词的语义既用作算术运算，又在布尔情况下用作量化。早在2001年，B. Courcelle、J.Makowsky和U. Rotics已经引入了一种形式主义，用于在Monadic二阶逻辑中定义的图参数，这里称为MSOLEVAL，其值在环R中。它们的框架可以很容易地适应于半环S。这种形式主义清楚地将逻辑部分与算术部分分开，并且也适用于词函数。本文给出了两个证明：值在S中的RMSOL和MSOLEVAL对词具有相同的表达能力。一个证明直接表明，MSOLEVAL捕获的功能可识别的加权自动机。另一个证明展示了如何将形式主义从一个转换成另一个。
2013-07-17 cs.FL cs.LO
Field Knowledge as a Dual to Distributed Knowledge: A Characterization by Weighted Modal Logic
本文通过加权模型将领域知识刻画为分布式知识的对偶，研究了由此产生的八种认知逻辑的相对表达力并建立了可靠完备的公理系统。
2024-06-30 cs.LO math.LO
A Rank-Preserving Gaifman Normal Form for First-Order Logic on Weighted Structures
Humboldt-Universität zu Berlin（柏林洪堡大学）；RWTH Aachen University（亚琛工业大学）
本文提出保秩Gaifman范式定理，适用于一阶逻辑及带模计数量词和加权结构逻辑ngFOW+，简化了无处稠密结构上近线性时间算法的元定理证明。
2026-09-30 cs.LO math.LO
Weight Assignment Logic
我们介绍了一个权重分配逻辑推理的数量语言的无限的话。该逻辑是经典MSO逻辑的扩展，并且允许描述具有多个权重参数的系统的定量性质，例如，回报与成本的比率我们表明，这种逻辑是表达等价于明确的加权Büchi自动机。我们还考虑了扩展的重量分配逻辑，这是表示等价于不确定性加权Büchi自动机。
2015-08-25 cs.FL cs.LO
Reasoning About Bounds in Weighted Transition Systems
本文提出一种推理加权转移系统中转移权重界限的方法，引入更粗的互模拟概念，并设计定制模态逻辑，证明其不变性、有限模型性质、完备公理化及可判定性。
2018-11-23 cs.FL cs.LO
Inference and learning in probabilistic logic programs using weighted Boolean formulas
KU Leuven（鲁汶大学）
概率逻辑程序是其中一些事实用概率注释的逻辑程序。本文研究了如何经典的推理和学习任务，从图形模型社区可以处理概率逻辑程序。概率逻辑程序以前没有真正解决过几个这样的任务，如计算给定证据的边缘和从（部分）解释中学习。本文的第一个贡献是为各种推理任务提供了一套有效的算法。它基于程序和查询以及证据到加权布尔公式的转换。这使我们能够将推理任务减少到经过充分研究的任务，例如加权模型计数，可以使用图形模型和知识编译文献中已知的最先进的方法来解决。第二个贡献是一个算法的参数估计的学习从解释设置。该算法采用期望最大化，并建立在顶部开发的推理算法。所提出的方法进行了实验评估。结果表明，推理算法提高了概率逻辑程序设计的最新水平，并且确实可以从解释中学习概率逻辑程序的参数。
2013-04-25 cs.AI cs.LG cs.LO
Parameterized Complexity of Weighted Team Definability
在这篇文章中，我们研究的复杂性加权团队可定义的逻辑与团队语义。这个问题是一个自然的模拟研究最多的问题之一，参数化的复杂性，加权Fagin定义的概念，这是制定在满足一阶公式与自由关系变量。我们专注于加权团队可定义性的参数化复杂性为一个固定的公式φ的中心团队为基础的逻辑。给定一个一阶结构A和参数值k作为输入，问题是确定A，T是否为某个规模为k的团队T建模phi。我们展示了几个结果，这个问题的依赖，独立和包含逻辑公式的复杂性。此外，我们还与加权团队定义的复杂性，在著名的W-层次结构以及paraNP的复杂性类。
2023-02-01 cs.CC cs.LO
Fuzzy propositional configuration logics
在De Morgan代数上引入并研究了一种加权命题配置逻辑。这种逻辑能够用定量特征来描述软件架构，例如架构中发生的交互的不确定性。我们通过证明每一个公式都可以写成一种特定的形式来处理我们逻辑中公式的等价问题。令人惊讶的是，有公式是等价的，只有在特定的德摩根代数。我们提供了我们的逻辑公式的例子，它描述了著名的软件架构配备了定量功能。
2021-11-28 cs.LO
Simulating Linear Logic in 1-Only Linear Logic
线性逻辑是由Girard作为经典逻辑的资源敏感的改进而引入的。事实证明，完全命题线性逻辑是不可判定的（Lincoln，Mitchell，Scedrov和Shankar），因此，它比（模态化的）经典或直觉主义逻辑更具表达力。在本文中，我们专注于研究线性逻辑的最简单的片段，如一个文字和常量只有片段（后者不包含文字在所有）。在这里，我们证明了线性逻辑的所有这些极其简单的片段（单文字，$\bot$ -only，甚至单位-only）与相应的完整版本具有完全相同的表达能力。我们还提出了一个完整的计算解释（在无循环程序与堆栈）的无底直觉线性逻辑。基于这种解释，我们证明了我们的编码的公平性，并建立上述复杂性的结果。
2017-09-09 cs.LO
A translation of weighted LTL formulas to weighted Büchi automata over ω-valuation monoids
本文在乘积$ω$ -赋值幺半群上引入了一个满足特定性质的加权LTL。我们还引入了带$\varepsilon$ -转移的加权广义Büchi自动机，以及在积$ω$ -赋值幺半群上带$\varepsilon$ -转移的加权Büchi自动机，并证明了这两个模型在表达上是等价的，也等价于文献中已经引入的加权Büchi自动机.我们证明了我们的逻辑的一个句法片段的每个公式可以有效地转化为一个加权的广义Büchi自动机与$\varepsilon$ -转移。对于满足特定性质的广义乘积$ω$ -赋值幺半群，我们定义了加权LTL，带$\varepsilon$ -变迁的加权广义Büchi自动机，带$\varepsilon$ -变迁的加权Büchi自动机，并证明了广义乘积$ω$ -赋值幺半群的上述结果.本文给出了一个带限制的语法片断的加权LTL公式到带$\varepsilon$ -转移的加权广义Büchi自动机的转化。
2022-01-02 cs.FL cs.LO
Nondeterministic Linear Logic
本文介绍了具有自对偶加法连接符的非确定性线性逻辑。在该系统中，证明网技术以自然的方式可用。重要的一点是，系统中的不确定性是通过规范化过程来表达的，而不是通过证明搜索。此外，我们还可以将该系统纳入J. - Y.Girard最近：非确定性轻线性逻辑和非确定性基本线性逻辑以一种非常自然的方式定义。
2004-10-14 cs.LO
P-time Completeness of Light Linear Logic and its Nondeterministic Extension
在CSL'99中，Roversi指出Girard的开创性论文“Light Linear Logic”中的图灵机编码有一个缺陷。此外，他提出了一个工作版本的编码轻仿射逻辑，但不是在轻线性逻辑。在本文中，我们提出了一个工作版本的编码轻线性逻辑。编码的想法是基于Girard的线性逻辑教程论文的评论。编码也是一个例子，显示了附加连接词的有用性。此外，我们还考虑了轻线性逻辑的非确定性扩展。我们证明了扩展系统是NP-完全的，其意义与轻型线性逻辑的P-完全性相同。
2004-10-18 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Super Exponentials in Linear Logic
根据次指数线性逻辑和分层有界线性逻辑的思想，我们提出了一个新的参数化版本的线性逻辑，它包含其他系统，如ELL，LLL或SLL，包括指数规则的变体。我们称这种系统为超指数线性逻辑（Superexponential Linear Logic，superLL）。通过对superLL的参数进行适当的约束，给出了割消元的一般性证明。这意味着线性逻辑的每一个变体，作为superLL的有效实例出现，也满足割消。
2021-12-30 cs.LO
Erratum to "Frequency Linear-time Temporal Logic"
我们修正了一个定理的证明，该定理表明频率线性时间时序逻辑的可满足性是不可判定的[TASE 2012]。
2020-10-01 cs.LO
Recursive querying of neural networks via weighted structures
RWTH Aachen University（亚琛工业大学）；Hasselt University（哈塞尔特大学）
本文提出了一种基于加权结构的递归查询方法，用于神经网络的验证与解释，展示了其在多项式时间内表达模型无关查询的能力，并证明了简单查询的计算复杂性。
2026-01-06 cs.AI cs.DB cs.LO
An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
微分线性逻辑丰富了线性逻辑与额外的逻辑规则的指数连接，对偶的通常规则的遗弃，削弱和收缩。本文提出了微分线性逻辑的证明网语法及其指称模型的范畴公理化。我们还介绍了一个简单的分类条件下，这些模型的一般反导数操作变得可用。最后，我们简要地描述了集合和关系的模型，并给出了有限性空间和线性和连续函数的模型更详细的说明。
2016-06-06 cs.LO
Using Z3 to Verify Inferences in Fragments of Linear Logic
本文提出一种基于Z3定理证明器的Gentzen风格线性逻辑矢列式模板，用于自动验证推理规则，并在MLL+Mix和MILL两个片段上验证了若干导出推理规则。
2023-09-25 cs.LO
WFA-IRL: Inverse Reinforcement Learning of Autonomous Behaviors Encoded as Weighted Finite Automata
University of California San Diego（加州大学圣地亚哥分校）
本文提出了一种从演示中学习逻辑任务规范和代价函数的方法。在自治系统中，手工构造规范对于复杂的目标和约束是具有挑战性的。相反，我们考虑演示任务执行，其逻辑结构和过渡成本需要推断的自主智能体。我们采用谱学习方法来提取加权有限自动机（WFA），近似未知的任务逻辑。此后，我们定义了一个产品之间的WFA高层次的任务指导和标记的马尔可夫决策过程的低层次的控制。逆强化学习（IRL）问题被认为是学习的成本函数通过反向传播代理和专家之间的行为通过规划算法的损失。我们提出的模型，称为WFA-IRL，是能够概括的执行推断任务规范在一套MiniGrid环境。
2022-09-19 cs.LG cs.LO
Quantum Algorithm for Multiplicative Linear Logic
本文描述了一种量子算法，用于线性逻辑子集的微积分中的证明搜索，使用Grover搜索算法。我们简要介绍了Grover搜索算法和线性逻辑，展示了算法的详细步骤，然后给出了在量子模拟器上获得的结果。
2023-02-17 cs.LO
Functional Interpretations of Intuitionistic Linear Logic
我们提出了三种不同的功能解释的直觉线性逻辑ILL，并显示这些对应于众所周知的功能解释的直觉逻辑IL通过嵌入IL到ILL。与第二作者以前的工作的主要区别是，在直觉线性逻辑（相对于经典线性逻辑）的解释！A是更简单的和同时的量词不再需要表征的解释。然后，我们比较我们的方法，在发展这三个证明的解释与德派瓦围绕辩证范畴模型的线性逻辑之一。
2011-03-24 cs.LO
A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology
线性蕴涵可以表示状态转移，但实际的转移系统是在时间、随机或概率约束下运行的，这些约束在普通线性逻辑中不能直接表示。我们提出了直觉线性逻辑的一般模态扩展，其中逻辑真值由约束索引，混合连接词将约束推理与逻辑推理相结合。该逻辑有一个集中的切免费的微积分，可以用来内化特定的约束过渡系统的规则，我们说明了这与同步随机π演算的充分编码。我们还提出了一些初步的实验，直接编码的生物系统的逻辑。
2013-10-16 cs.LO
Unifying Graded Linear Logic and Differential Operators
CNRS（法国国家科学研究中心）
本文提出了一种将格度线性逻辑与微分算子结合的逻辑体系，并给出了其指派模型。
2026-01-08 cs.LO
A Short Note on Two-Variable Logic with a Linear Order Successor and a Preorder Successor
证明了由线性序后继和预序后继扩展的二元逻辑的有限可满足性问题是不可判定的。
2013-06-14 cs.LO
The succinctness of first-order logic on linear orders
简洁性是比较不同逻辑的强度的一种自然的衡量标准。直观地说，如果所有可以在L_2中表示的性质都可以在L_1中用（大约）相同大小的公式表示，但某些性质可以在L_1中用（明显）更小的公式表示，则逻辑L_1比另一逻辑L_2更简洁。我们研究线性序上逻辑的简洁性。我们的第一个定理是关于一阶逻辑的有限变量片断的。证明了：（1）在多项式因子下，一阶逻辑的2-和3-变量片段在线性序上具有相同的简洁性。(ii)4变量片段比3变量片段以指数方式更简洁。我们的第二个主要结果比较了线性序上的一阶逻辑与一元二阶逻辑的简洁性。我们证明了一元二阶逻辑的片段在线性序上具有与一阶逻辑相同的表达性，但非初等地比一阶逻辑更简洁。
2006-03-08 cs.LO
Mackey-complete spaces and power series -- A topological model of Differential Linear Logic
本文描述了直觉主义线性逻辑的一个指称模型，它也是一个微分范畴。公式被解释为Mackey-完备拓扑向量空间，线性证明被解释为有界线性函数。为了解释线性逻辑的非线性证明，我们使用了麦基完备空间之间的幂级数的概念，推广了C语言中整函数的概念。最后，我们得到了直觉主义微分线性逻辑的一个定量模型，其中的句法微分对应于通常的微分，证明的解释满足泰勒展开分解。
2015-07-12 cs.LO
Surface Proofs for Nonsymmetric Linear Logic (Extended Abstract)
证明了乘性线性逻辑中的一个证明可以表示为一个修饰曲面，使得两个证明仅当它们的曲面在几何上等价时，它们在逻辑上等价。这是arXiv的扩展摘要：1601.05372。
2017-01-18 cs.LO
Introduction to linear logic and ludics, part I
《线性逻辑和态极逻辑引论》一文概述了由Girard分别于1986和2001所创建的线性逻辑和态极逻辑.这两种理论都从第一原理重新审视了数理逻辑，并从计算机科学中得到了启发和应用。本文第一部分介绍了线性逻辑的联结词和证明规则，线性逻辑的可判定性属性及其模型。文章的第二部分将研究证明网并简要介绍态极逻辑.证明网是证明的图式表示,是线性逻辑的主要创新之一.
2005-01-18 cs.LO
An Intuitionistic Linear Logical Semantics of SAND Attack Trees
本文介绍了直觉线性逻辑中SAND攻击树的一种新的逻辑基础。这个新的基础是基于一个新的逻辑称为攻击树线性逻辑（ATLL）。在介绍ATLL之前，我们给出了几种新的攻击树逻辑模型，第一种是基于真值表的攻击树逻辑模型。然后，我们把这种语义提升为一种基于线性的攻击树语义，它引入了蕴涵，但这可以进一步提升为ATLL所基于的辩证模型。ATLL的一个重要特征是它支持顺序合取的完全分布性。
2018-01-21 cs.LO
An Abstract Approach to Stratification in Linear Logic
我们研究分层的概念，用于子系统的线性逻辑与低复杂性界限上的削减消除程序（所谓的轻逻辑），从抽象的角度来看，引入一个逻辑系统，其中分层是由一个单独的模态处理。这种模态是吉拉德的轻线性逻辑的段落模态的概括，它产生于一种适用于线性逻辑所有模型的一般范畴结构。因此，我们了解到，分层可以制定独立的指数模态;当它被迫连接到指数模态，它产生有趣的复杂性属性。特别是，从我们的分析干三个替代的重新制定的Baillot和Mazza的线性逻辑的水平：一个几何，一个互动，一个语义。
2013-02-14 cs.LO
Introduction to linear logic and ludics, part II
本文是《线性逻辑和态极逻辑引论》一文的第二部分。它致力于证明网络，在有限的，但中心，框架的乘法线性逻辑和ludics，这是最近发展的目的是进一步揭示基本的互动性质的计算和逻辑。我们希望本文能对这一新的理论带来一些计算机科学方面的启示。
2005-01-19 cs.LO
A Gödel Calculus for Linear Temporal Logic
我们考虑哥德尔时序逻辑（$\sf GTL$），一个变种的线性时序逻辑的基础上哥德尔-达米特命题逻辑。在最近的工作中，我们已经表明，这种逻辑享受自然语义作为一个模糊逻辑和作为一个超直觉逻辑。使用语义学方法，证明了该逻辑是{ \sc pspace}-完全的。在本文中，我们提供了一个演绎演算$\sf GTL$，并表明这种演算是健全的和完整的上述语义。
2022-05-10 cs.LO
Satisfiability for two-variable logic with two successor relations on finite linear orders
本文研究了两个二元关系和两个二元关系的一阶逻辑的有限可满足性问题，它对应于两个有限线性序的导出后继关系。我们证明了这个问题在NEXPTIME中是可判定的。
2013-10-18 cs.LO
Weighted Rules under the Stable Model Semantics
School of Computing, Informatics and Decision Systems Engineering（计算、信息与决策系统工程学院）
本文提出加权规则概念以克服稳定模型语义的确定性，解决答案集程序中的矛盾、对稳定模型进行排名、赋予概率以及应用统计推断计算加权稳定模型。
2026-05-10 cs.AI 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
A note on undecidability of propositional non-associative linear logics
本文介绍了一种非结合、非交换的命题直觉线性逻辑，称为命题非结合非交换直觉线性逻辑（NACILL）。我们证明了NACILL和它的任何扩展的交换和/或压缩规则是不可判定的。此外，我们介绍了两种类型的经典版本的NACILL，即，NACILL的对合版本和NACILL的循环和对合版本。我们证明这两个逻辑也是不可判定的。
2019-09-30 cs.LO
Weighted First Order Model Counting for Two-variable Logic with Axioms on Two Relations
本文研究二变量逻辑在多个关系公理扩展下的加权一阶模型计数复杂性，证明两个线性序或两个无环关系时FO^2的WFOMC为#P_1难，并给出C^2带线性序及两个后继关系的多项式时间算法。
2025-08-15 cs.AI cs.LO
Automata Linear Dynamic Logic on Finite Traces
本文提出有限迹上的自动机线性动态逻辑（ALDL_f），通过结合命题逻辑与非确定性有限自动机表达时序约束，在保持PSPACE复杂度的同时获得了等价于一元二阶逻辑的表达能力提升。
2025-07-10 cs.LO
Cofree coalgebras and differential linear logic
证明了向量空间中直觉线性逻辑的语义也是微分线性逻辑的一个模型，并且证明了上自由余代数的笛卡尔闭范畴是简单型微分λ演算的一个模型.
2019-01-07 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
An Indexed Linear Logic for Idempotent Intersection Types (Long version)
引入Indexed Linear Logic的幂等变体，通过基变换重构语法并利用子类型关系实现幂等性，证明其作为逻辑能细化经典线性逻辑且切消过程终止并合流。
2024-02-15 cs.LO
The relational model is injective for Multiplicative Exponential Linear Logic
本文证明了乘性指数线性逻辑（MELL）的一个完备性结果：证明了关系模型对于MELL证明网是单射的，即关系模型中MELL证明网之间的相等性是用割消法精确公理化的。
2016-05-10 cs.LO
A Hybrid Linear Logic for Constrained Transition Systems
线性蕴涵可以表示状态转移，但实际的转移系统是在时间、随机或概率约束下运行的，这些约束在普通线性逻辑中不能直接表示。我们提出了直觉线性逻辑的一般模态扩展，其中逻辑真值由约束索引，混合连接词将约束推理与逻辑推理相结合。该逻辑有一个集中的切免费的微积分，可以用来内化特定的约束过渡系统的规则，我们说明了这与同步随机π演算的充分编码。
2016-03-08 cs.LO
Linear Temporal Justification Logics with Past Operators
本研究将Artemov证明逻辑与含过去、未来算子的线性时序逻辑结合，构建多种时序证立逻辑并证明其可靠性与完备性，还探究了证立与时间的交互原理。
2021-09-28 cs.LO
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
本文给出了基本正规时态逻辑Kt的一个线性嵌套演算。我们表明，演算，使向后证明搜索，反模型建设和句法切割消除。因此，线性嵌套序列提供了为包含逆的模态逻辑提供足够的证明理论所需的最小嵌套量。作为奖励，这产生了对称模态逻辑KB的无切演算。
2019-07-02 cs.LO
Bounded Linear Logic, Revisited
我们提出QBAL，Girard，Scedrov和Scott的有界线性逻辑的扩展。该系统的主要新颖之处是量化资源变量的可能性。这种推广使得有界线性逻辑更加灵活，同时在多项式时间内保持可靠性和完备性。特别是，我们提供了合成嵌入Leivant的RRW和霍夫曼的LFPL到QBAL。
2010-12-23 cs.LO
The ILLTP Library for Intuitionistic Linear Logic
使用标准化问题集对自动定理证明（ATP）系统进行基准测试是一种用于测量其性能的成熟方法。然而，这种库的非经典逻辑的可用性是非常有限的。在这项工作中，我们提出了一个库基准吉拉德的（命题）直觉线性逻辑。为了快速引导问题的集合，并讨论相关问题的选择和理解它们作为线性逻辑定理的意义，我们使用Kleene直觉定理集合在传统专著“元数学导论”中的翻译。我们分析了四种不同的翻译直觉逻辑线性逻辑和比较他们的证明使用线性逻辑为基础的证明与聚焦。为了增强我们库中的问题集，我们将这三个保持可靠性的翻译应用于ILTP库中的命题基准。最后，我们产生了一个全面的可达性问题的Petri网和编码等问题的线性逻辑序列，从而扩大了我们的问题集。
2019-04-15 cs.LO
