Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
路径检查是模型检验问题的一种特殊情况，其中所考虑的模型是单个路径，在监视、测试和验证中起着重要的作用。我们证明了线性时间时序逻辑（LTL），路径检查可以有效地并行化。除了核心逻辑，我们考虑扩展的LTL与有界未来（BLTL）和过去的时间（LTL+过去）运营商。尽管这两个扩展都以指数方式提高了逻辑的简洁性，但路径检查仍然可以有效地并行化：我们对LTL、LTL+Past和BLTL+Past的算法是在AC ^1（logDCFL）\subseteq NC中。
2012-10-19 cs.LO
Hybrid Branching-Time Logics
混合分支时间逻辑被引入作为状态变量和向下箭头绑定器的CTL类逻辑的扩展。根据最近的工作在线性框架，只有一个单一的变量逻辑被认为是。研究了结果逻辑的表达能力和可满足性的复杂性。作为主要结果，证明了几个分支时间逻辑的混合形式的可满足性问题是2 EXPTIME-完全的。这些分支时间逻辑的范围从CTL的严格片段到CTL的扩展，可以谈论过去并表达公平性。相对于CTL的复杂性差距解释了相应的简洁性结果。为了证明这个上界，将分支时间逻辑的自动机理论方法推广到混合逻辑，证明了交替单卵石Buchi树自动机的非空性是2 EXPTIME-完全的。
2007-08-13 cs.CC cs.LO
Separateness of Variables -- A Novel Perspective on Decidable First-Order Fragments
经典的决策问题，正如今天所理解的那样，是基于优雅的句法标准，寻求一阶逻辑的可判定部分和不可判定部分之间的划分。在本文中，我们处理的概念，分离的变量，并探讨其适用于经典的决策问题。在一个给定的公式中，两个不相交的一阶变量集合是分离的，如果来自这两个集合的变量从未在该公式的任何原子中共存。这个简单的概念有助于扩展许多著名的可判定的一阶片段显着，并在某种程度上保持可判定性。我们将证明，对于几个前缀片段，几个保护片段，两个变量片段，和凹槽片段。总之，我们将更仔细地研究九个这样的扩展。有趣的是，它们中的每一个都包含关系一元一阶片段而不相等。虽然扩展表现出与各自的原件相同的表达能力，但某些逻辑属性可以更简洁地表达。在三种情况下，简洁性差距不能使用任何初等函数来界定。
2019-11-26 cs.LO
Simulating Linear Logic in 1-Only Linear Logic
线性逻辑是由Girard作为经典逻辑的资源敏感的改进而引入的。事实证明，完全命题线性逻辑是不可判定的（Lincoln，Mitchell，Scedrov和Shankar），因此，它比（模态化的）经典或直觉主义逻辑更具表达力。在本文中，我们专注于研究线性逻辑的最简单的片段，如一个文字和常量只有片段（后者不包含文字在所有）。在这里，我们证明了线性逻辑的所有这些极其简单的片段（单文字，$\bot$ -only，甚至单位-only）与相应的完整版本具有完全相同的表达能力。我们还提出了一个完整的计算解释（在无循环程序与堆栈）的无底直觉线性逻辑。基于这种解释，我们证明了我们的编码的公平性，并建立上述复杂性的结果。
2017-09-09 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
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
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
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
A note on undecidability of propositional non-associative linear logics
本文介绍了一种非结合、非交换的命题直觉线性逻辑，称为命题非结合非交换直觉线性逻辑（NACILL）。我们证明了NACILL和它的任何扩展的交换和/或压缩规则是不可判定的。此外，我们介绍了两种类型的经典版本的NACILL，即，NACILL的对合版本和NACILL的循环和对合版本。我们证明这两个逻辑也是不可判定的。
2019-09-30 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
ExpTime Tableaux for the Description Logic SHIQ Based on Global State Caching and Integer Linear Feasibility Checking
我们给出了第一个ExpTime（复杂性最优）的Tableau决策过程，用于检查描述逻辑SHIQ中的知识库的可满足性，当数字以一元编码时。我们的程序是基于全局状态缓存和整数线性可行性检查。
2013-12-31 cs.LO
A New Linear Time Correctness Condition for Multiplicative Linear Logic
本文给出了无单位乘法线性逻辑证明网的一个新的线性时间正确性条件。我们的方法是基于重写系统的树。我们只有三条重写规则。与以前的线性时间正确性条件相比，我们的系统是令人惊讶的简单和直观的吸引力。
2020-11-23 cs.LO
Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules
我们的手稿研究线性时间（与UNTIL和NEXT）逻辑的基础上的概念不传递时间。非传递时间特别是，我们展示了如何在这样的框架中表示知识的概念（在这里，我们认为逻辑操作NN和操作UNTIL（实际上，时间整体）是针对过去）。我们研究的基本数学问题是任何逻辑系统的基本问题-可判定性和可判定性w.r.t.可接受的规则首先，我们考虑具有非一致非传递性的逻辑，并描述如何解决这种逻辑的可判定性问题。然后，我们考虑了这种逻辑的一种修改--具有一致不传递性的线性时态逻辑，并解决了推理规则的可容许性问题。在论文的结论部分列举了一系列有待解决的问题。
2015-03-30 cs.LO
Categorical Proof Theory of Co-Intuitionistic Linear Logic
为了给余直觉主义逻辑提供范畴语义，人们必须面对特里斯坦·克罗拉德（Tristan Crolard）指出的事实，即把余指数定义为余积的集合在范畴集合中不起作用，其中余积是不相交的并集。遵循熟悉的直觉线性逻辑模型的构造与指数”！“，我们在具有附加结构的对称monoidal左闭范畴中建立了余直觉逻辑的模型，在自由范畴的构造中使用Crolard对余直觉逻辑的项赋值的一个变体.
2014-09-19 cs.LO
Resolution in Linguistic First Order Logic based on Linear Symmetrical Hedge Algebra
本文研究了真值取自线性对称对冲代数的语言一阶逻辑的归结问题。我们建立语言一阶逻辑的基本组成部分，包括语法和语义。我们提出了一个解决原则，我们的逻辑解决两个子句具有矛盾的语言真值。由于语言信息是不确定的，语言逻辑中的推理是近似的。因此，我们引入了可靠性的概念，以捕捉自然近似的归结推理规则。
2014-03-30 cs.LO
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
有限迹上的时态逻辑与潜在无限迹上的时态逻辑不同。Rozelu首先证明了有限迹上线性时态逻辑（LTLf）的完备性，并提出了一个新的共归纳公理。我们提供了一个不同的证明，用更少，更传统的公理。我们的证明是Kröger和Merz的Henkin-Hasenjaeger式证明的直接改编。我们修改的本质是我们“注入”有限性：也就是说，我们改变证明结构以确保模型是有限的。我们的目标是提出一个全面的，可访问的证据。
2021-07-13 cs.LO
A Fibrational Perspective on Differential Linear Logic
Université Sorbonne Paris Nord, LIPN, CNRS, UMR 7030（巴黎北大学，LIPN，法国国家科学研究中心，UMR 7030）
本文从纤维视角出发，将微分线性逻辑的范畴模型表示为带有切线 functor 的纤维对，为统一 DILL 和依赖类型奠定基础。
2026-05-08 cs.LO
Linear-time logics -- a coalgebraic perspective
本文从余代数视角提出一种通用框架，通过结合分支行为与线性行为类型来定义线性时间逻辑，并证明其逐步语义与基于路径的语义等价，从而支持对定量系统中线性时间性质的可能性、似然性或最小代价进行推理。
2024-06-12 cs.LO
Jets and differential linear logic
证明了固定光滑流形上的向量丛范畴及其相应的方便模范畴是直觉微分线性逻辑的模型。指数模态的建模是由组成射流comonad，其Kleisli范畴具有线性微分算子作为态射，与更熟悉的分布comonad，其Kleisli范畴具有光滑映射作为态射。结合这两个comonads给出了微分线性逻辑的语义的一个新的解释，其中Kleisli态射是光滑的局部泛函，或者等价地，光滑的偏微分算子，并且codereliction映射诱导泛函导数。这指向一个逻辑，因此计算理论的非线性偏微分方程及其解决方案的基础上变分。
2019-12-28 cs.LO
Weak topologies for Linear Logic
本文构造了线性逻辑的一个指称模型，其对象是所有局部凸的、可分离的拓扑向量空间，并赋予它们弱拓扑。否定被解释为对偶，线性证明被解释为连续线性函数，非线性证明被解释为单项式序列。我们并不是通过双正交运算来完成我们的构造。这就产生了一种从拓扑学角度对连接词极性的解释。
2016-03-07 cs.LO
Linear Non-Transitive Temporal Logic, Knowledge Operations, Algorithms for Admissibility
本文研究了非传递时态线性逻辑LTL（Past，m）中推理规则的可满足性、可判定性和可容许性、知识概念和主体知识等问题。我们发现算法解决上述问题，证明我们的方法考虑线性非传递时间与几个例子。主要的、最复杂的、技术上的新结果是LTL（Past，m）w.r.t.可接受的规则我们讨论了几种方法来形式化的知识和代理的知识在给定的方法在非传递线性逻辑模型指向过去的概念。
2014-06-11 cs.LO
Elementary Logic in Linear Space
一阶逻辑通常被认为是在基本量化的环境中进行演绎的研究。在本文中，我们采取另一个有利的位置，并概念化一阶逻辑作为一个线性空间，编码的“可扩展性”。而演绎观点强调如何（即，过程），空间视角强调在哪里（即，位置）。我们探讨了几个后果的角度转变为“信号在空间”的一阶逻辑，包括（1）基于正交分解的证明的概念，（2）分配概率的句子，反映逻辑的不确定性的方法，和（3）“模型作为边界”的原则，涉及到理论的模型，其“大小”。
2020-01-30 cs.LO
A gentle introduction to Girard's Transcendental Syntax for the linear logician
从技术上讲，先验语法是关于设计具有计算基础的逻辑。它提出了一个新的证明理论框架，其中逻辑（证明，公式，真理，......）并不比计算更原始。所有的逻辑实体和活动都将在给定的计算模型上以格式化/结构化的形式呈现，该模型应尽可能通用，简单和自然。先验语法中逻辑的选择基础是一种我称之为“恒星解析”的计算模型，它基本上是罗宾逊一阶子句解析的无逻辑重构，具有与瓦片系统相关的动态。先验语法的一个初始目标是从这个新框架中恢复线性逻辑。特别地，该模型自然地编码证明结构的切割消除。通过使用“交互式类型”的思想，让人想起可实现性理论，可以设计公式/类型来概括线性逻辑的连接词。由于交互式类型，我们能够达到一个语义自由的空间，正确性标准被视为测试（如在单元测试或模型检验）证明逻辑正确性，从而允许有效地使用逻辑实体。
2022-04-05 cs.LO
Relating Reasoning Methodologies in Linear Logic and Process Algebra
我们发现，逻辑前序的证明理论的概念相吻合的上下文前序的过程理论的概念，从公式作为过程的解释的线性逻辑片段的CCS样演算。该论点利用进程代数中的其他标准概念，即标记的转换系统和共归纳定义的模拟关系。这一结果建立了一种方法之间的联系，以原因有关的过程规范和方法，原因有关的逻辑规范。
2012-11-17 cs.LO
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
2015-06-08 cs.LO
Games and Full Completeness for Multiplicative Linear Logic
我们提出了一个游戏语义的线性逻辑，其中公式表示游戏和证明表示获胜的策略。我们表明，我们的语义产生一个范畴模型的线性逻辑和证明完全完备的乘法线性逻辑与MIX规则：每一个获胜的策略是一个独特的无割证明网的表示。{ \em history-free}策略的概念扮演了一个关键的角色;在无历史策略和交互作用几何之间建立了强有力的联系。我们的语义学结合了极性的自然概念，导致了添加剂的精细处理。我们与Joyal，Blass等人的相关工作进行了比较。
2013-11-23 cs.LO
Towards an embedding of Graph Transformation in Intuitionistic Linear Logic
线性逻辑已经被证明能够在一个声明性的框架中嵌入基于重写的方法和处理演算。在本文中，我们正在探索嵌入的双推出图转换到量化的线性逻辑，导致Curry-Howard风格的同构之间的图形和转换，一方面，公式和证明条款。利用图的线性蕴涵表示规则和可达性，以及图和变换的张量模型并行合成，我们得到了一种能够对图变换系统及其计算进行编码和性质推理的语言.
2009-11-29 cs.LO
Cut Elimination in Multifocused Linear Logic
我们研究切消除的多焦点变体的全线性逻辑在微积分。多焦点范式的证明产生的问题，不出现在一个标准的聚焦系统，有关的限制，在分组规则的情况下，在聚焦阶段。我们表明，削减消除可以在一个明智的方式，即使证明需要一些特定的引理来处理多聚焦阶段，并讨论与削减消除时所产生的困难，考虑范式的证明在线性逻辑。
2015-02-17 cs.LO
Resolution in Linguistic Propositional Logic based on Linear Symmetrical Hedge Algebra
本文介绍了一个命题语言逻辑，作为自动不确定推理的语言信息的基础。首先，我们建立了一个基于线性对称对冲代数的真值域语言逻辑系统。然后，我们考虑哥德尔的t-范数和t-连接词来定义我们逻辑的逻辑连接词。接下来，我们提出了一个决议推理规则，其中两个条款有矛盾的语言真值可以解决。我们还给出了可靠性的概念，以捕捉的近似性质的决议推理规则。最后，我们提出了一个解决方案的最大可靠性。
2013-07-30 cs.LO
