From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics
本文将线性套序列和2-序列的方法推广到自然演绎中。公式用空间坐标装饰，允许按照自然演绎的原始精神制定形式系统--每个连接词只有一个引入和一个消除规则，没有额外的（结构）规则，没有明确引用预期的可及性关系克里普克模型。我们给出了从K到S4的正规模态逻辑系统。对于系统的直观版本，我们定义了证明约简，并证明了证明规范化，从而获得了一致性的语法证明。对于逻辑K和K4，我们使用存在谓词（遵循Scott）来制定合理的演绎规则。
2021-04-24 cs.LO
On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
我们考虑两种风格的证明演算紧张的逻辑，在嵌套序列的基础上提出的形式主义的家庭。一个嵌套的序列可以看作是一个传统的单边序列树。我们的第一种演算风格被称为“浅演算”，其中推理规则仅应用于嵌套的根节点中的根结点。我们的浅层演算是鹿岛演算的时态逻辑的扩展，并与显示演算共享一个基本特征，即存在被称为“显示公设”的结构规则。浅层结石有一个简单的切割消除程序，但由于存在显示假设和其他结构规则，不适合进行证据搜索。第二种类型的演算使用深度推理，推理规则可以应用于嵌套的递归中的任何节点。我们表明，对于一系列的扩展时态逻辑，这两种风格的演算是等价的，并且有一个自然的证明理论之间的对应关系显示公设和深推理。深度推理演算具有子公式性质，没有显示公设或其他结构规则，这使得它们成为一个更好的证明搜索框架。
2011-05-14 cs.LO
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Technische Universität Dresden（德累斯顿工业大学）
本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。
2026-03-31 cs.LO
Automata with Nested Pebbles Capture First-Order Logic with Transitive Closure
在（确定性）对数空间中可识别的字符串语言的特征是双向（确定性）多头自动机，或者遵循Immerman，具有（确定性）传递闭包的一阶逻辑。在这里，我们详细阐述了这个结果，并匹配的头的数量传递闭包的arity。更确切地说，具有k元确定性传递闭包的一阶逻辑与具有k个头的确定性自动机在其输入上行走具有相同的能力，另外使用有限的嵌套卵石集。这个结果对于字符串、有序树以及具有固定自动机的图族都是有效的，该自动机可用于遍历图族中每个图的节点。此类族的其他示例包括轴网、圆环和矩形迷宫。对于非确定性自动机，逻辑仅限于传递闭包的正出现。树的k=1的特殊情况表明，具有嵌套卵石的单头确定性树行走自动机具有一元确定性传递闭包的一阶逻辑特征。这改进了我们先前的结果，将这些自动机之间的一阶和一元二阶逻辑树。
2007-04-26 cs.LO
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
本文针对可证性逻辑GL切割消去终止性证明困难的问题，提出基于嵌套矢列式的语法化切割消去方法，并借鉴Kushida（2020）的思想，仅用直接归纳避免额外度量和复杂重写，从而消除Poggiolesi（2009）证明中的歧义。
2024-12-31 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
A robust class of languages of 2-nested words
正则嵌套词语言（Regular Nested Word Languages）可见下推语言）严格地扩展了常规单词语言，同时保留了它们的主要闭包和可判定性属性。以前的工作已经表明，考虑2-嵌套词的语言，即用两个匹配丰富的词（a.k.a. 2-显然下推语言），并不成功：相应的自动机模型在确定性下并不封闭。在这项工作中，受同态表示的索引语言，我们确定了一个子类的2嵌套的话，我们称之为2波的话。这个类严格地扩展了嵌套单词的类，同时保留了它的主要属性。更确切地说，我们证明了相应的自动机模型的确定性下的封闭性，我们提供了一个逻辑特征的识别语言，并表明相应的图有界树宽。因此，我们得到重要的封闭性和可判定性。最后，我们证明了我们定义的语言的词投影属于线性索引语言类。
2022-08-22 cs.FL cs.LO
On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
本文研究了命题直觉主义逻辑、一阶非常数论域直觉主义逻辑和一阶常数论域直觉主义逻辑的标号演算和套演算之间的关系。它示出，拟合的嵌套结石自然产生于其相应的标记结石-为上述每一个逻辑-通过消除标记派生的结构规则。这两种类型的系统之间的平移对应关系被用来表明嵌套演算从其相关的标记演算中继承了证明理论属性，例如规则的完整性，可逆性和切割容许性。由于标记的演算很容易通过逻辑的语义，本文提出的方法可以被看作是一个，从而细化版本的标记演算（包含嵌套的演算片段）具有良好的性能直接从逻辑的语义。
2021-04-19 cs.LO math.LO
Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics
本文通过引入线性规则和可达性规则，并推广嵌套矢列以包含签名，为命题及一阶Gödel-Dummett逻辑构建了具有高度保持可逆性、可靠且无割完备的嵌套矢列系统，同时为更广泛的中间逻辑提供了无割嵌套矢列系统的构造思路。
2024-06-06 cs.LO math.LO
Nested Hoare Triples and Frame Rules for Higher-order Store
分离逻辑是一种霍尔风格的逻辑，用于对具有堆分配的可变数据结构的程序进行推理。作为一个步骤，扩展分离逻辑的高级语言ML风格的一般（高阶）存储，我们调查的兼容性嵌套霍尔三元组与几个变化的高阶框架规则。嵌套三元组和框架规则的相互作用可能是微妙的，并且包含某些框架规则实际上是不合理的。一个特定的规则组合可以通过克里普克模型来证明是一致的，在克里普克模型中，世界生活在一个递归定义的超度量空间中。由此产生的逻辑允许我们优雅地证明涉及存储代码的程序。特别是，使用递归定义的断言，它导致了自然的规范和通过存储处理递归所需的不变量的证明。
2011-09-27 cs.LO
A Polynomial Translation of Logic Programs with Nested Expressions into Disjunctive Logic Programs: Preliminary Report
嵌套逻辑程序最近被引入，以便允许在答案集语义下的逻辑程序规则的头部和主体中的任意嵌套公式。嵌套表达式可以不受限制地使用合取、析取以及作为失败操作符的否定来形成。这为知识表示和推理提供了一个非常灵活和紧凑的框架。已有的结果表明，嵌套逻辑程序可以初等地转化为标准（非嵌套）析取逻辑程序，只需对体文字应用否定作为失败算子.这是非常实际的相关性，因为它允许我们评估嵌套的逻辑程序的手段，现成的析取逻辑编程系统，如DLV。然而，事实证明，这种简单的转换在最坏的情况下会导致指数爆破，尽管复杂性结果表明两种形式主义之间存在多项式转换。在本文中，我们接受了这一挑战，并提供了一个多项式的逻辑程序与嵌套表达式转换为析取逻辑程序。此外，我们表明，这种翻译是模块化的和（强）忠实。我们已经实现了简单的和高级的转换;生成的编译器作为DLV的前端，并在Web上公开提供。
2002-07-19 cs.AI cs.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.LO
Nested Sequents for Provability Logic GLP
本文提出了一种基于嵌套相继式的可证性逻辑GLP证明系统，证明了切消定理，并以此在语法上将GLP归约为其重要片段J。
2014-10-24 cs.LO math.LO
Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 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
Nested Sequents for Quasi-transitive Modal Logics
本文针对带拟传递性公理的模态逻辑，基于嵌套矢列式提出构造性切割消去程序，并给出替代性的模块化证明系统表述。
2024-06-13 cs.LO math.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
本研究提出一种基于无切割嵌套序列演算的纯句法方法，证明含逆模态的经典时态逻辑及其扩展、双直觉主义逻辑的Craig插值性质，创新引入定义插值元对偶的正交性条件，无需语义或嵌入辅助。
2023-06-14 cs.LO math.LO
A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
本文为直觉主义模态逻辑 IK 提出无标签双嵌套矢列演算，支持判定、由失败证明直接构造有限反模型，并可模拟现有嵌套与标签演算。
2025-05-13 cs.LO
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.LO
Nested Words for Order-2 Pushdown Systems
研究了2阶可折叠的高阶下推系统（CPDS）对带有push/pop匹配关系的MSO和PDL（propositional dynamic logic with converse and loop）的线性时间模型检验.为了捕捉这些线性时间行为与匹配，我们提出了2阶嵌套的话。这些图由一个词结构与两个二进制匹配关系，一个堆栈的每一个顺序，这与相应的堆栈上的匹配弹出（或折叠）推增强。由于匹配关系，可满足性和模型检验是不可判定的。因此，我们提出了一个欠近似，限制1阶推送可以弹出的次数。利用这种下近似，它仍然允许无限的堆栈高度，我们得到的可满足性和模型检验的MSO和PDL的可判定性。问题是PDL的ExpTime-Complete。
2016-09-20 cs.FL cs.LO
Nested Sequents for First-Order Modal Logics via Reachability Rules
本研究提出首个支持多种论域与路径条件的一阶模态逻辑无切割嵌套矢列系统，通过可达性规则与结构精化方法构建，证明了结构精化可扩展至一阶模态逻辑领域。
2023-11-08 cs.LO math.LO
Nested Sequents
我们看到如何嵌套序列，超序列的自然概括，使我们能够开发一个系统的模态逻辑证明理论。与其他突出的形式主义，如显示演算和标记序列相反，嵌套序列留在模态语言中，并允许在字面意义上享受子公式属性的证明系统。在第一部分中，我们研究了一套系统的嵌套系统的所有正常模态逻辑形成的一些组合的公理的序列性，自反性，对称性，传递性和欧几里德。我们建立健全性和完整性和他们的一些良好的性质，如可逆的所有规则，结构规则的可接受性，终止证明搜索，以及句法切割消除。在第二部分中，我们研究了常识逻辑，一种具有不动点模态的模态逻辑。我们期待在两个无穷证明系统，这种逻辑：现有的一个普通序列的基础上，没有语法切割消除程序是已知的，和一个新的嵌套序列的基础上。我们看到如何嵌套的序列，在普通的序列相比，允许句法削减消除，从而使我们能够获得一个序数上限的长度证明。
2010-04-11 cs.LO math.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。
2025-12-03 cs.DM cs.LO math.LO
The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract)
本文研究了判定嵌套模拟语义模态逻辑中特征公式的复杂性，证明了素公式判定在2-嵌套模拟下为coNP完全，在n>=3时为PSPACE完全。
2025-09-17 cs.LO
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO math.LO
Synthesis for prefix first-order logic on data words
本文研究了无限参与者分布式系统的反应式合成问题，通过数据字建模执行，并采用实现有限顺序的前缀一阶逻辑片段作为规范，最终证明了该合成问题的可判定性。
2024-04-22 cs.LO
Temporal Logics on Words with Multiple Data Values
本文提出并研究了属性词的时态逻辑，即在每个位置具有（有限）（属性，值）对集合的数据词。它认为一个基本的逻辑是一个语义片段的逻辑$LTL^\downarrow_1$的Demri和Lazic与运营商导航到未来和过去。通过对数据自动机的空性问题的简化，证明了这种基本逻辑是可判定的。虽然基本逻辑只允许导航到出现固定数据值的位置，但扩展也允许导航到具有不同数据值的位置。除了一些不可判定的结果外，还证明了具有不等式目标条件的UNTIL算子的扩张是可判定的。
2010-10-06 cs.LO
Logic of Awareness for Nested Knowledge
本文提出了带划分与链的意识逻辑（ALPC），通过引入不可区分关系和意识的信念链来形式化有限推理能力智能体的嵌套显式知识，并提供了Kripke风格语义、完备的证明系统及其在计算机科学和博弈论中的应用展望。
2024-02-13 cs.LO cs.MA
Logic Column 11: The Finite and the Infinite in Temporal Logic
本文研究了有限和无限序列上的LTL时态算子的解释。这是用来作为一个健全的和完整的公理化的Caret，最近的时间逻辑推理嵌套过程调用和返回的程序推导的基础。
2005-04-24 cs.LO
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
在这项工作中，我们考虑的可满足性问题的逻辑，结合字方程的字符串变量表示的话的无限长度，正则语言的话属于Presburger限制的话的长度。我们提出了一种新的决策过程，在两个可决策的片段，包括二次字方程（即，每个字符串变量最多出现两次）。所提出的过程减少了问题解决的Presburger算法的可满足性。该过程结合了两个主要组成部分：（i）一个算法，以获得一个完整的一组所有的解决方案的词方程和正则表达式的连接;和（ii）两种方法，以精确计算关系约束的字符串长度所隐含的所有solutions.We已经实现了一个原型工具，并评估了一组可满足性问题的逻辑。实验结果表明，该工具是有效和高效的。
2018-05-23 cs.LO
An Application of the Feferman-Vaught Theorem to Automata and Logics for<br> Words over an Infinite Alphabet
我们表明，一个特殊的情况下，Feferman-Vaught组合定理产生了一个自然的概念，自动机的有限字在一个无限的字母表，具有良好的封闭性和可判定性，以及一些逻辑刻画。我们还考虑了一个轻微的扩展的Feferman-Vaught形式主义，它允许表达更多的组件值之间的关系（如平等），并证明相关的可判定性结果。从这个结果，我们得到了新的类的可判定逻辑的词在一个无限的字母表。
2008-03-25 cs.LO
A Kruskal Decision Procedure for Intuitionistic Modal Logic IK4
Scuola Normale Superiore（意大利高等师范学院）
该研究提出了直觉模态逻辑IK4的Kruskal判定程序，通过无切嵌套证明结合Kruskal定理等证明其可判定性，给出了统一的证明高度界。
2026-08-12 cs.LO
Two-Variable Logic for Hierarchically Partitioned and Ordered Data
本文研究了分层结构数据下的二变量逻辑，证明了其有限可满足性问题的复杂性，并展示了不同变体的可判定性结果。
2025-12-10 cs.LO
Verifying Graph Programs with First-Order Logic (Extended Version)
我们认为霍尔式验证的图形程序设计语言GP 2。在以前的工作中，图形属性指定的所谓的E-条件，扩展嵌套的图形条件。然而，这种类型的断言对于习惯于标准一阶逻辑中的形式化规范的程序员来说并不容易理解。在本文中，我们提出了一种方法来验证GP 2程序与一个标准的一阶逻辑。我们展示了如何构建一个最强的自由后置条件的规则模式和先决条件。然后我们扩展了这个构造以获得任意无循环程序的最强自由后置条件。与以前的工作相比，这允许的原因是一个非常普遍的类图程序。特别是，许多程序与嵌套循环可以验证新的演算。
2020-11-03 cs.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.LO
Verifying Graph Programs with First-Order Logic
我们认为霍尔式验证的图形程序设计语言GP 2。在以前的工作中，图形属性指定的所谓的E-条件，扩展嵌套的图形条件。然而，这种类型的断言对于习惯于标准一阶逻辑中的形式化规范的程序员来说并不容易理解。在本文中，我们提出了一种方法来验证GP 2程序与一个标准的一阶逻辑。我们展示了如何构建一个最强的自由后置条件的规则模式和先决条件。然后，我们扩展这个建设，以获得最强的自由后置条件的任意无循环程序。与以前的工作相比，这允许的原因是一个非常普遍的类图程序。特别是，许多程序与嵌套循环可以验证新的演算。
2020-12-03 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
First-Order Logic on Higher-Order Nested Pushdown Trees
我们引入了一个新的层次结构的高阶嵌套下推树推广的Gesar等人。的嵌套下推树概念。嵌套下推树是一种非常有用的控制流表示方法，可以用来验证递归调用一阶函数的程序。高阶嵌套下推树是由高阶下推系统生成的图的展开的扩展。此外，一类嵌套的下推树的水平n是一致的一阶解释的水平n+1的可折叠的下推图类。高阶下推图类和可折叠高阶下推图类之间的关系还不是很清楚。我们希望通过对嵌套下推树层次结构的进一步研究，能够更好地理解这两种层次结构。本文研究了高阶嵌套下推树的一阶模型检验问题。我们表明，一阶模型检验的前两个层次上的层次结构是可判定的。此外，我们还得到了一类一级嵌套下推树的2-EXPSPACE算法。证明技术涉及到一个伪本地分析的策略，在两个相同的副本嵌套下推树的Escherichfeucht-Fraisse游戏。普通的局部性参数在Gaifman引理的精神不适用于这里，因为嵌套的下推树往往有小直径。我们引入了相关祖先的概念，它提供了一个足够的描述的FO_k型的每个元素在一个高阶嵌套下推树。这些祖先的本地分析，使我们能够证明存在的限制性获胜策略的Escherichfeucht-Fraisse游戏。然后，这些策略被用来创建一个一阶模型检验算法。
2012-02-09 cs.FL cs.LO math.LO
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
2015-08-10 cs.LO math.LO
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
Nested Regular Path Queries in Description Logics
CNRS（法国国家科学研究中心）；Univ. Paris Sud（巴黎第十一大学）；Free Univ. of Bozen-Bolzano（博尔扎诺自由大学）；Vienna Univ. of Technology（维也纳工业大学）
双向规则路径查询（2 RPQ）最近受到越来越多的关注，因为它们能够通过灵活地导航图结构数据来关联对象对。它们出现在SPARQL 1.1（新的标准RDF查询语言）和XML查询语言中的属性路径中。在符合ESTA，我们认为2 RPQ的扩展与嵌套，它允许一个要求，沿路径的对象满足复杂的条件，反过来表示通过（嵌套）2 RPQ。本文研究了在描述逻辑中表达领域知识的情况下，回答嵌套2 RPQ及其合取（CN 2 RPQ）的计算复杂性。我们建立严格的复杂性界限的数据和各种DL的组合复杂性，从轻量级DL（DL-Lite，EL）的高度表达的。有趣的是，我们能够证明，向（C）2 RPQ添加嵌套不会影响任何所考虑的DL的查询应答的最坏情况数据复杂度。然而，在轻量级DL的情况下，将嵌套添加到2 RPQ会导致组合复杂性的惊人跳跃，从P-完全到Exp-complete。
2014-03-04 cs.AI cs.DB cs.LO
Automating Reasoning with Standpoint Logic via Nested Sequents
TU Dresden（德累斯顿工业大学）
立场逻辑是最近提出的形式主义的背景下，知识的整合，它提倡一个多视角的方法，允许推理的选择不同的，可能相互冲突的立场，而不是强迫他们的统一。在本文中，我们介绍了嵌套的立场逻辑-证明系统，操纵树的节点是多套公式-并展示了如何自动化的立场推理的非确定性证明搜索算法。为了获得最坏情况下的复杂性最优的证明搜索，我们介绍了一种新的技术，在嵌套序列的上下文中，被称为“着色”，其中包括一个公式作为输入，猜测一定的着色其子公式，然后运行证明搜索在嵌套的递归演算上的彩色输入。我们的技术可以让我们决定的有效性，在CoNP的立场公式，因为证明搜索只产生一个部分的证明相对于每个允许的着色的输入。我们展示了如何将所有部分证明融合在一起，以构建一个完整的证明时，输入是有效的，以及如何某些部分证明可以转化为一个反模型时，输入是无效的。这些“证明”（即证明和反模型）作为输入有效性的解释。
2022-05-05 cs.AI cs.DS cs.LO
Structural Morphisms for Nested Conditions - Full Version
University of Twente（特温特大学）；University of Pisa（比萨大学）
本文针对用于约束图变换规则适用性的嵌套条件，引入模拟逻辑联结词的算子，提出结构态射概念并研究其与条件蕴含的一致性，在范畴论语境下证明相关操作的函子性与泛性质。
2026-08-13 cs.LO
Timed context-free temporal logics (extended version)
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（ECNTL）和嵌套度量时序逻辑（NMTL）。ECNTL逻辑是CARET逻辑（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。我们证明了ECNTL的可满足性和可视下推时间自动机VPTA对ECNTL的可视模型检验是可判定的和EXPTIME完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于ECNTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-08-14 cs.LO
A First-Order Complete Temporal Logic for Structured Context-Free Languages
本文提出一种基于算子优先级语言的新时序逻辑POTL，证明其FO完备性，优于NWTL和OPTL，支持前置/后置条件、栈检查等需求，并配套模型检测工具。
2022-07-28 cs.LO
Extending Büchi Automata with Constraints on Data Values
最近，数据树和数据字在XML推理和系统验证方面受到了相当大的关注。这些是树或词，除了来自有限字母表的标签之外，还携带来自无限字母表的数据值（数据）。一般来说，很难获得足够表达的数据字和树的逻辑，但对于可满足性问题仍然具有合理的复杂性。在本文中，我们扩展和研究的概念，Büchi自动机的欧米茄字的数据。我们证明了这种扩张的空性问题在初等复杂性下是可判定的。然后，我们应用我们的结果来显示两种逻辑的可判定性的欧米茄字的数据：一阶逻辑的两个变量的片段和一些经典的线性时序逻辑的欧米茄字的数据的扩展。
2012-06-23 cs.LO
Regular expressions over countable words
本文将经典正则语言理论扩展至可数字设定，引入并研究五类正则表达式，证明其与逻辑和代数刻画的表达等价性，从而推广了形式语言理论的基础结果。
2025-05-02 cs.LO
POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages
模型检验程序的问题促进了对上下文无关结构推理的时态逻辑定义的研究。其中最值得注意的是嵌套词的时态逻辑，如CaRet和NWTL。最近，基于操作符先后次序语言（OPL）类的逻辑OPTL被引入，它比嵌套字更强大。我们定义了新的基于OPL的逻辑POTL，证明了它的FO-完全性，并提供了一个模型检验过程。POTL改进了NWTL，使制定的要求，涉及前/后条件，堆栈检查，和其他的异常结构的存在。它在OPTL的基础上进行了改进，因为它是FO完备的，并且更容易表达堆栈检查和函数局部属性。
2020-10-31 cs.FL cs.LO
Duality for the existential fragment of first-order logic on words with numerical predicates of a fixed arity
这篇文章适合于研究拓扑对偶方法在理论计算机科学中的应用。这种方法的最终目标之一是通过研究表征它们的适当拓扑对象来推导计算复杂性理论的结果。把这两个看似分离的领域联系起来的纽带是逻辑，更确切地说，是有限模型理论的一个子域，称为词的逻辑。它允许将复杂性类描述为有限字母表上的某些语言家族，可能是非正则的。很少有人知道的对偶理论相对于片段的一阶逻辑的话，这是范围以外的正则语言。我们的工作的贡献是这样一个片段的详细研究。固定一个整数$k \geq 1$，我们考虑布尔代数$\mathcal{B}Σ_1[\mathcal{N}^{u}_k]$。它对应于由句子的布尔组合组成的词的逻辑片段，所述句子通过使用至多$k$存在量词、字母谓词和arity $l \in \{1,...,k\}$的统一数值谓词的块来定义。本文对任意$k \geq 1$的布尔代数的对偶空间进行了详细的研究，并给出了它的点的几个刻画。在$k=1$的特殊情况下，我们能够构造一族超滤子方程，它们刻画了布尔代数$\mathcal{B} Σ_1[\mathcal{N}^{u}_1]$。我们使用拓扑方法，以证明这些方程是健全的和完整的关于我们提到的布尔代数。
2022-01-03 cs.LO
A Decidable Class of Nested Iterated Schemata (extended version)
Grenoble University（格勒诺布尔大学）；CNRS（法国国家科学研究中心）
许多问题可以通过依赖于参数的命题公式的模式来指定，例如，电路的规格通常取决于其输入的位数。我们定义了一个逻辑的公式，称为“迭代图式”，允许表达这样的模式。图式用索引命题（如P_i，P_i+1，P_1）和广义连接词（如/i=1）扩展命题逻辑。n或i=1.. n（称为“迭代”），其中n是称为“参数”的（未绑定）整数变量。迭代模式的表达能力严格地大于命题逻辑：它甚至超出了一阶逻辑的范围。我们定义了一个证明过程，称为DPLL*，可以证明一个模式是满足至少一个值的参数，在精神的DPLL过程。然而，相反的问题，即证明模式对于参数的每个值都是不可满足的，是不可判定的，所以DPLL* 一般不会终止。尽管如此，我们证明，它终止的语法子类称为“定期嵌套”的模式。这是第一个非平凡类，DPLL* 被证明终止。此外，规则嵌套模式的类是第一个允许迭代嵌套的可判定类，即允许模式的形式/n =1.。n（/ \j =1.. n.）。
2010-01-24 cs.AI cs.LO
Timed Context-Free Temporal Logics
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（EC_NTL）和嵌套度量时序逻辑（NMTL）。逻辑EC_NTL是逻辑CaRet（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。本文证明了EC_NTL的可满足性和可视下推时间自动机（VPTA）对EC_NTL的可视模型检验是可判定的和EXPTIME-完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于EC_NTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
2018-09-10 cs.LO
