Visibly Linear Dynamic Logic
我们介绍了可见线性动态逻辑（VLDL），它扩展了线性时态逻辑（LTL）的时间运营商，由可见的下推语言在有限的字。在VLDL中，例如，表示函数在执行后将变量重置为原始值，即使存在无限数量的中间递归调用。我们证明了VLDL精确地描述了$ω$ -可视下推语言。因此，它比LTL更严格地表达，并且能够表达具有无限调用堆栈的程序的递归特性。这项工作的主要技术贡献是一个翻译的VLDL到$ω$ -明显下推自动机的指数大小通过单向交替跳跃自动机。这种转换产生指数时间算法的可满足性，有效性，和模型检验。我们还表明，明显的下推游戏VLDL获胜的条件是可解的三次方指数时间。我们证明了所有这些问题是完整的，为各自的复杂性类。
2017-05-17 cs.FL cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
On the Expressive Power of 2-Stack Visibly Pushdown Automata
可见下推自动机是输入驱动的下推自动机，它可以识别一些非正则上下文无关语言，同时保持了有限自动机的良好闭包和可判定性。具有多个堆栈的可见下推自动机最近被La Torre，Madhusudan和Parlato考虑，他们进一步利用可见性的概念来获得丰富的自动机类，甚至可以表达上下文无关语言之外的属性。同时，它们的自动机在布尔运算下是封闭的，具有可判定的空性和包含性问题，并且在具有额外嵌套结构的词上享有一元二阶逻辑的逻辑表征。这些结果需要一个限制版本的明显下推自动机与多个堆栈，其行为可以分为一个固定数量的阶段。在本文中，我们考虑2-栈可见下推自动机（即，具有两个堆栈的可视下推自动机）以其不受限制的形式。我们表明，他们是表达等价的一元二阶逻辑的存在片段。此外，我们还发现一元二阶量词交替在多重嵌套的词中形成了一个无限的层级结构。结合这些结果，我们得出结论，2-栈可见下推自动机是不封闭的补充。最后，我们讨论了Büchi 2-栈可见下推自动机运行在无限（嵌套）的话的表达能力。通过无限量词扩展逻辑，我们同样可以建立与存在一元二阶逻辑的等价。
2008-12-24 cs.LO
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
本文提出时序逻辑NTL，用于推理动态下推网络中递归程序的调用、返回及动态线程创建行为，并证明其模型检测与可满足性问题的复杂度不高于下推系统上的LTL，为验证此类程序提供了新途径。
2023-10-30 cs.FL cs.LO
Logics for Context-free Hyperproperties
Technische Universität Ilmenau（伊尔梅瑙工业大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学，法国国家科学研究中心，信息研究与研究所）；Aalborg University（奥尔堡大学）
提出一种用于指定上下文无关超性质的逻辑，通过迹量化扩展可视下推自动机，并证明单量词交替下的模型检测可判定性及不可判定性边界。
2026-10-04 cs.FL cs.LO
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 cs.LO
POPACheck: A Model Checker for Probabilistic Pushdown Automata
TU Wien（维也纳工业大学）
POPACheck 是一种用于概率下推自动机的模型检查工具，支持时序逻辑规范，能处理概率程序的行为验证。
2025-06-04 cs.LO
Computational Complexity of Model-Checking Quantum Pushdown Systems
本文研究了量子栈系统模型检查的计算复杂性，证明了量子栈系统在特定逻辑下的可判定性，并展示了其NP难性。
2026-08-10 cs.CC cs.LO
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
我们调查的表达能力的两种主要类型的程序逻辑复杂的，非常规的程序属性在文献中发现：那些扩展命题动态逻辑（PDL），和那些扩展模态μ演算。这是受到最近发现的一种可判定程序逻辑的启发，这种逻辑被称为具有Chop的可见下推定点逻辑，它将模态μ演算和PDL扩展到可见下推语言上，到目前为止，这构成了可判定程序逻辑的两个支柱。在这里，我们表明这个逻辑不仅比它的两个片段中的任何一个更具表达力，而且事实上比它们的结合更具表达力。因此，程序逻辑之间的可判定性边界已经被适当地推高。我们完成了图片提供的结果分离所有的PDL为基础的和模态不动点逻辑与定期，明显下推和任意上下文无关的建设。
2021-08-24 cs.LO
Reasoning about strategies on collapsible pushdown arenas with imperfect information
不完全信息策略逻辑（Strategy Logic with Imperfect Information，SLiR）是一种非常具有表现力的逻辑，旨在表达分布式系统中策略能力的复杂属性。SLiR以前的工作集中在有限系统，并表明，模型检查问题是可判定的，当系统的控制状态的信息是分层的球员或系统的组件，这意味着球员或组件可以完全根据他们各自的状态知识排序。我们表明，从有限到无限的系统产生的可折叠（高阶）下推系统保留可判定性，自然的限制下，堆栈内容是可见的。证明遵循与有限系统相同的路线，但需要使用（可折叠）交替下推树自动机。这种自动机是不可判定的，但半交替下推树自动机被引入并证明是可判定的，研究了两个局中人下推系统的策略问题。为了解决多个球员的层次信息，我们进一步完善这些自动机：我们定义方向引导（可折叠）下推树自动机，并表明它们是稳定的投影，非确定性和缩小。对于后一种操作，用于处理不完美的信息，稳定性在某些假设下保持，当用于具有可见堆栈的系统时，该假设是满足的。然后，我们使用这些自动机来证明我们的主要结果。
2020-07-30 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 Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL 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
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
Nested Sequents for Provability Logic GLP
本文提出了一种基于嵌套相继式的可证性逻辑GLP证明系统，证明了切消定理，并以此在语法上将GLP归约为其重要片段J。
2014-10-24 cs.LO math.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
Nested Sequents for Quantified Modal Logics
本文针对带不同论域的量化模态逻辑构建嵌套序列演算，证明其具备良好结构性质、与公理系统等价且可靠完备，并说明存在谓词可表达时演算具有内部性。
2023-11-08 cs.LO math.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
Weighted Logics for Nested Words and Algebraic Formal Power Series
嵌套词是由Madhusudan和Alfred提出的一种递归程序模型，近年来引起了人们的广泛兴趣。本文引入了半环的数量扩张，研究了半环中的嵌套词元素的嵌套词列。我们表明，经常嵌套的字系列符合系列定义的加权逻辑介绍Droste和Gastin。为此，我们建立了一个嵌套的话和自由bisemigroup之间的连接。应用我们的结果，我们得到了代数形式幂级数的加权逻辑刻画。这推广了Lautemann，Schwentick和Therien关于上下文无关语言的结果。
2010-02-19 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
Probabilistic regular graphs
确定性图文法生成规则图，形成下推系统的配置图的结构扩展。本文研究了正则图的概率扩张，它是通过概率标记图文法的端弧而得到的。这些图的随机特性表示使用PCTL，计算树逻辑的概率扩展。我们在这里提出了一个算法进行近似验证的PCTL公式。此外，我们证明了概率正则图上PCTL的精确模型检验问题是不可判定的，除非限制到定性性质。我们的研究结果概括了EKM 06，概率下推自动机，使用类似的方法结合图形语法技术。
2010-11-01 cs.FL cs.LO
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。
2025-12-03 cs.DM cs.LO math.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
On Nested Sequents for Constructive Modal Logics
我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。
2015-09-02 cs.LO
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
语法逻辑是指多模态逻辑K的扩展，其中模态公理从形式语法生成。我们考虑一个证明理论，在嵌套微积分，与逆，即，语法逻辑，每个模态算子[a]都有一个逆。扩展以前的作品嵌套的tense逻辑系统，我们表明所有的语法逻辑（有或没有逆）可以在嵌套的tense演算，其中的公理是内在的演算作为结构规则的形式化。这些结石的语法切割消除证明使用类似的程序显示逻辑。如果文法是上下文无关的，那么可以摆脱所有的结构规则，支持深度推理和额外的传播规则。我们给出了一个新的半决策过程的上下文无关文法逻辑，使用嵌套的深度推理演算，并表明，在给定的上下文无关文法是正规的情况下，这个过程终止。与文献中所有其他现有的决策程序的规则文法逻辑，我们的程序不假设一个有限状态自动机编码的公理。
2012-04-11 cs.LO
Finitary semantics of linear logic and higher-order model-checking
在本文中，我们解释了如何高阶模型检验和线性逻辑之间的连接最近展出的作者导致一个新的和概念上启发性的证明选择问题最初建立的Carayol和塞尔使用可折叠的下推自动机。其主要思想是从一个无限的和有色的关系语义已经制定了的的BiddayY演算，并取代它的有限对应的基础上有限素代数格。给定一个高阶递归方案G，其在模型中解释的有限性使我们能够将一个新的高阶递归方案G_phi与任何MSO公式φ联系起来，解决选择问题。
2015-05-01 cs.LO math.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
First-Order and Temporal Logics for Nested Words
嵌套字是过程程序中执行路径的结构化模型，反映了它们的调用和返回嵌套结构。有限嵌套字还捕获解析树和其他树结构数据（如XML）的结构。我们提供了新的时间逻辑的有限和无限嵌套的话，这是自然的扩展LTL，并证明这些逻辑是一阶表示完全的。其中之一是基于添加一个“内”的模态，评估一个子字的公式，以前研究的递归状态机（RSM）的验证属性的上下文中的逻辑CaRet。另一种逻辑NWTL基于使用线性和嵌套结构的摘要路径的概念。对于NWTL，我们证明了可满足性是EXPTIME-完全的，并且模型检查可以在RSM模型的大小的时间多项式中进行，并且在NWTL公式的大小中是指数的（并且也是EXPTIME-完全的）。最后，证明了嵌套词上的一阶逻辑具有三变量性质，并给出了一个嵌套词的时态逻辑，它对于一阶二变量片断是完备的。
2011-03-03 cs.LO
A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus
本文引入了由前向汇合 Kripke 模型刻画的自然直觉主义模态逻辑 FIK，为其提供了完备的 Hilbert 风格公理化和双嵌套演算，该演算兼具判定程序与有限反模型提取功能。
2023-09-12 cs.LO
Modularisation of Sequent Calculi for Normal and Non-normal Modalities
在这项工作中，我们探讨之间的连接（线性）嵌套的微积分和普通的微积分正常和非正常模态逻辑。通过提出本地版本的普通的正则化规则，我们得到线性嵌套正则化演算的一些逻辑，包括我们所知的第一个嵌套正则化演算的一个大类的简单依赖的多模态逻辑，和许多标准的非正常模态逻辑。由此产生的系统是模块化的，并有单独的左，右介绍规则的方式，这使得他们服从规范的双极条款。虽然这种颗粒的的证明搜索规则引入了更多的选择，我们展示了如何线性嵌套的证明演算可以限制到阻塞的推导，直接对应于普通的证明推导。
2017-11-16 cs.LO math.LO
Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
本文将非周期性、无星性和一阶可定义性的经典等价关系扩展至算子优先语言，通过引入OP表达式和文法变换完成证明，并指出该方法同样适用于可见下推语言。
2023-11-21 cs.FL cs.LO
Nested-sequent Calculus for Modal Logic MB
本文针对模态逻辑 MB 的完全性与可判定性未决问题，构造了其嵌套矢列演算并加以解决，同时探讨了添加新模态符号后的逻辑 MB+。
2024-12-31 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
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
Refining Labelled Systems for Modal and Constructive Logics with Applications
Australian National University（澳大利亚国立大学）；Laboratoire d’informatique de l’École polytechnique（巴黎综合理工学院计算机实验室）
本文介绍了“结构精化方法”，它作为一种手段转换的模态和/或建设性逻辑的关系语义到一个“经济”的证明系统，通过连接两个证明理论的范式：标记和嵌套演算。标记序列的形式主义已经成功地在拥有理想的证明理论的性质，可以自动生成大型类的逻辑切割免费演算。尽管有这些品质，标记系统使用了复杂的语法，明确地结合了相关逻辑的语义，这样的系统通常违反了子公式属性的高度。相比之下，嵌套微积分使用更简单的语法，并坚持严格阅读子公式属性，使这样的系统在自动推理算法的设计中非常有用。然而，嵌套演算范式的缺点是，关于这种演算的自动构造（如在标记设置中）的一般理论基本上是不存在的，这意味着嵌套系统的构造和它们的属性的确认通常是在个案的基础上完成的。细化方法连接这两种范式在一个富有成效的方式，通过转换成嵌套的（或，精制标记）系统与前保持整个转换过程中的属性标记系统。为了证明精化的方法和它的一些应用，我们考虑文法逻辑，一阶直觉逻辑和道义STIT逻辑。介绍了细化标记演算将被用来提供第一个证明搜索算法的道义STIT逻辑。此外，我们使用我们的精炼标记演算的语法逻辑，以表明在类中的每一个逻辑具有有效的林登插值属性。
2021-07-30 cs.AI cs.DM cs.FL
On a Non-Context-Free Extension of PDL
在过去的25年里，人们在寻找命题动态逻辑（PDL）的可判定非正则扩展方面做了大量的工作。直到最近，PDL的表达扩展，允许可见下推自动机（VPAs）作为一种形式主义来描述程序，被引入并证明有一个确定性的双指数时间的可满足性问题完成。最近，VPA形式主义被扩展到所谓的k-阶段多栈可见下推自动机（k-MFPAs）。与VPA类似，已经表明k-MVPAs的语言具有期望的有效闭包属性，并且空性问题是可判定的。在引入k-MPPA之际，有人问，用k-MPPA扩展PDL是否仍然导致可判定逻辑。这个问题在这里得到了否定的回答。我们已经证明了，对于PDL的扩展与2阶段MPPA与两个堆栈的可满足性成为1^_1^1-完全。
2007-07-18 cs.LO
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
2015-08-10 cs.LO math.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
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
Automating Reasoning with Standpoint Logic via Nested Sequents
TU Dresden（德累斯顿工业大学）
立场逻辑是最近提出的形式主义的背景下，知识的整合，它提倡一个多视角的方法，允许推理的选择不同的，可能相互冲突的立场，而不是强迫他们的统一。在本文中，我们介绍了嵌套的立场逻辑-证明系统，操纵树的节点是多套公式-并展示了如何自动化的立场推理的非确定性证明搜索算法。为了获得最坏情况下的复杂性最优的证明搜索，我们介绍了一种新的技术，在嵌套序列的上下文中，被称为“着色”，其中包括一个公式作为输入，猜测一定的着色其子公式，然后运行证明搜索在嵌套的递归演算上的彩色输入。我们的技术可以让我们决定的有效性，在CoNP的立场公式，因为证明搜索只产生一个部分的证明相对于每个允许的着色的输入。我们展示了如何将所有部分证明融合在一起，以构建一个完整的证明时，输入是有效的，以及如何某些部分证明可以转化为一个反模型时，输入是无效的。这些“证明”（即证明和反模型）作为输入有效性的解释。
2022-05-05 cs.AI cs.DS cs.LO
Nested Hoare Triples and Frame Rules for Higher-order Store
分离逻辑是一种霍尔风格的逻辑，用于对具有堆分配的可变数据结构的程序进行推理。作为一个步骤，扩展分离逻辑的高级语言ML风格的一般（高阶）存储，我们调查的兼容性嵌套霍尔三元组与几个变化的高阶框架规则。嵌套三元组和框架规则的相互作用可能是微妙的，并且包含某些框架规则实际上是不合理的。一个特定的规则组合可以通过克里普克模型来证明是一致的，在克里普克模型中，世界生活在一个递归定义的超度量空间中。由此产生的逻辑允许我们优雅地证明涉及存储代码的程序。特别是，使用递归定义的断言，它导致了自然的规范和通过存储处理递归所需的不变量的证明。
2011-09-27 cs.LO
Inducing syntactic cut-elimination for indexed nested sequents
本文通过建立标记相继式与索引嵌套相继式的对应关系，为索引嵌套相继式演算引入句法切割消去证明，并首次为中间逻辑构造了无切割的索引嵌套相继式演算。
2018-11-23 cs.LO
Logic of Awareness for Nested Knowledge
本文提出了带划分与链的意识逻辑（ALPC），通过引入不可区分关系和意识的信念链来形式化有限推理能力智能体的嵌套显式知识，并提供了Kripke风格语义、完备的证明系统及其在计算机科学和博弈论中的应用展望。
2024-02-13 cs.LO cs.MA
A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
本文为直觉主义模态逻辑 IK 提出无标签双嵌套矢列演算，支持判定、由失败证明直接构造有限反模型，并可模拟现有嵌套与标签演算。
2025-05-13 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
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
Technische Universität Dresden（德累斯顿工业大学）
研究哥德尔-勒布可证性逻辑的多个相继式形式体系间证明的互译性。通过重组树形超相继式证明及引入‘线性化技术’解决问题，获首个无切割线性嵌套相继式演算，建立各系统间证明对应关系。
2026-07-07 cs.LO math.LO
