Optimal Tableau Decision Procedures for PDL
Institute of Informatics, University of Warsaw（华沙大学信息学研究所）
本文将Pratt关于PDL中公式集可满足性检验的表判定过程重新表述。我们的提法更简单，更直接，便于执行。扩展的方法，我们给出了第一个EXPTIME（最佳）的tableau决策过程不基于转换的一致性检查的ABox w.r.t. PDL中的TBox（这里，PDL被视为描述逻辑）。证明了PDL中实例检验问题的数据复杂性是coNP-完全的。
2009-06-01 cs.AI cs.CC cs.LO
An ExpTime Procedure for Description Logic $\mathcal{ALCQI}$ (Draft)
针对$\mathcal{ALCQI}$中的可满足性问题，给出了一个基于ExpTime表的最坏情况决策过程。一般公理
2007-03-18 cs.LO
EXPTIME Tableaux for the Coalgebraic mu-Calculus
模态逻辑的共代数方法提供了一个统一的框架，它可以捕获结构上不同的模态逻辑的语义，包括分级和概率模态逻辑和联盟逻辑。在本文中，我们介绍了coalgebraic μ演算，一般（coalgebraic）框架的扩展与不动点算子。我们的主要结果是相关的Tableau演算的完整性和EXPTIME的可判定性守护公式。从技术上讲，这是通过将可满足性减少到非良基场景的存在来实现的，而非良基场景的存在又相当于平价博弈中获胜策略的存在。我们的结果是参数的基础类的模型和产量，作为具体的应用，以前未知的复杂性界限的概率μ演算和扩展的联盟逻辑与不动点。
2011-08-09 cs.LO math.LO
Tableaux for Dynamic Logic of Propositional Assignments
CRIL, Univ. of Artois and CNRS（阿尔图瓦大学与法国国家科学研究中心CRIL实验室）；IRIT, Univ. of Toulouse and CNRS（图卢兹大学与法国国家科学研究中心IRIT研究所）
动态命题推理逻辑（DL-PA）是近年来研究的命题动态逻辑（PDL）的一种替代方案。在DL-PA中，PDL的抽象原子程序被命题变量到真值的赋值所取代。这使得DL-PA具有PDL所没有的一些有趣的元逻辑性质，如Kleene星的可消除性、紧性和插值性。我们定义和分析tableaux演算DL-PA，并表明它符合已知的复杂性结果。
2014-06-09 cs.AI cs.LO
Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
本文给出了一个最优的（EXPTIME）、可靠的和完全的基于表的判定逆命题动态逻辑（CPDL）可满足性的算法，该算法不需要使用解析割。我们的主要贡献是一个健全的methodto结合我们以前的最佳方法跟踪最少不动点的PDL与我们以前的最佳方法处理逆的描述逻辑ALCI。扩展是不平凡的，因为这两个方法不能简单地组合。我们提供了足够的细节，以便其他人能够实现。我们的OCaml实现似乎是CPDL的第一个定理证明器。
2010-04-15 cs.LO
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
University of Amsterdam（阿姆斯特丹大学）；University of Groningen（格罗宁根大学）
本文解决了悬而未决的PDL Craig插值问题，基于Borzechowski的硕士论文提出循环表方法，构造性证明插值性质并给出Haskell实现，还提及Lean形式化验证的相关工作。
2026-11-02 cs.LO math.LO
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities
我们提出了一个简单的理论解释的建设和正确性的增量和最坏情况下的模态逻辑的最佳决策过程与不测。该程序给出了一个抽象的重要方面的Goré和Widmann的PDL证明。从一个输入公式开始，该过程会生成一个Pratt样式的图形表，直到该表证明或否定该公式的可满足性。该程序提供了一个基础，实际证明，因为可满足性和不可满足性的公式，往往可以确定与小tableaux。
2012-09-06 cs.LO
Complexity and expressivity of propositional dynamic logics with finitely many variables
研究了命题动态逻辑有限变量片段可满足性的复杂性。我们认为三种形式主义属于三个代表性的复杂性类，广泛理解，-经常PDL，这是EXPTIME-完整的，PDL的交集，这是2 EXPTIME-完整的，PDL与并行组合，这是不可判定的。我们表明，对于这些逻辑中的每一个，即使我们只允许仅由命题常量（即没有命题变量）构建的公式作为输入，可满足性的复杂性也保持不变。此外，我们表明，这是一个后果的丰富的表达能力的变量免费片段：对于所有的逻辑，我们认为，这样的片段是整个逻辑的语义表达。我们推测，这是PDL风格的代表，以及密切相关的逻辑。
2019-01-18 cs.LO math.LO
Predicative proof theory of PDL and basic applications
提出了一种Schütte模式的命题动态逻辑（PDL），它是单边半形式树型演算Seq $_ω^{\text{pdl}}$，带有标准割规则和带有主公式$\left[ P^{\ast }\right] \!A$的omega规则. Seq $_{ω}^{\text{pdl}}$中的无ω规则导子是有限的（树），并且由这些有限导子可推导的序列在PDL中是有效的。此外，Seq $_ω^{\text{pdl}}$的割消定理在Peano算术（PA）中是可证明的，该Peano算术（PA）通过超限归纳扩展到Veblen的序数$φ_ω\left( 0\right) $。因此（通过无割子公式性质）PA的这种谓词扩展证明了任何给定的$\left[ P^{\ast }\right] $ -free序列在PDL中是有效的，当且仅当它在Seq $_ω^{\text{pdl}}$中可通过有限的无割和ω-规则推导来推导，而任意无星序列的PDL-有效性在多项式空间中是可判定的。前者也意味着标准的Herbrand风格的结论，这最终导致$S$的PDL-有效性的PSPACE-可判定性，只要$P$是原子的并且$A$是在合适的\emph{basic conjunctive normal form}中。此外，我们考虑在对偶\emph{basic disjunctive normal form}中的无星公式$A$，以及相应的展开式$S…
2021-02-23 cs.CC cs.LO
Towards Finite Satisfiability of PDL with Loops
Institute of Logic and Computation, TU Wien（逻辑与计算研究所，维也纳工业大学）；Computer Science Department, University of Wrocław（计算机系，弗罗茨瓦夫大学）
本文针对带循环的命题动态逻辑（LPDL）有限可满足性问题，证明了特定限制下其有限可满足性为ExpTime完全，通过双向树自动机与ω-正则可折叠条件实现了有限模型的构造。
2026-10-14 cs.LO
The Complexity of the Constructive Master Modality
本文提出了两种构造性主模态逻辑，并证明其复杂性为 EXPTIME，同时解决了相关逻辑的有效性问题
2026-07-22 cs.LO math.LO
Complexity of the Description Logic ALCM
University of Leicester（莱斯特大学）
本文证明了描述逻辑ALCM中知识库的一致性检验问题是ExpTime完全的。M代表Motz，Rohrer和Severi定义的元建模。为了展示我们的主要结果，我们定义了ExpTime Tableau算法作为Nguyen和Szalas在ALC中检查知识库一致性的算法的扩展。
2015-11-12 cs.AI cs.LO
PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse
Univ. Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）；Bordeaux INP（波尔多国立理工学院）；Univ. Buenos Aires（布宜诺斯艾利斯大学）；CONICET-UBA（阿根廷国家科学与技术研究理事会-布宜诺斯艾利斯大学联合机构）
本文提出严格强于 ICPDL、CQ 和 CRPQ 的表达性逻辑 CPDL+，按公式树宽分层，并用带石子互模拟博弈刻画其表达力，证明固定树宽下可满足性为 2ExpTime、模型检测为 Ptime。
2023-04-20 cs.AI cs.DB cs.LO
Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge
我们开发了一个基于增量表的决策过程的多智能体认知逻辑MAEL（CD）（又名S5_n（CD）），其语言包含运营商的个人知识的代理有限集Ag，以及运营商的分布和共同的知识在Ag的所有代理。我们的tableau程序工作在（确定性）指数时间，从而建立了一个上限MAEL（CD）-可满足性，匹配（隐式）下限已知从早期的结果，这意味着ExpTime-完整的MAEL（CD）-可满足性。因此，我们的程序提供了一个复杂的最佳算法检查MAEL（CD）-可满足性，然而，在大多数情况下，是更有效的。我们证明了该方法的可靠性和完备性，并举例说明。
2008-08-29 cs.LO cs.MA
Robustness of Constraint Automata for Description Logics with Concrete Domains
提出基于约束自动机的方法，通过符号约束扩展转移，在具体域满足简单性质时实现EXPTIME最优上界，并证明本体一致性问题的EXPTIME隶属度，扩展至逆角色、功能角色名和约束断言仍保持该复杂度。
2026-06-29 cs.AI cs.LO
A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation First-order Logic
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR5800（波尔多大学）；Universidad de Buenos Aires, FCEN, DC & CONICET-UBA, ICC（布宜诺斯艾利斯大学）
本文研究了UCPDL+逻辑，其包含PDL扩展、连接查询和单目否定一阶逻辑，探讨了其表达能力、可满足性和模型检查问题。
2026-10-20 cs.DB cs.LO
The Inverse Method Implements the Automata Approach for Modal Satisfiability
基于表格的模态和描述逻辑的可满足性判定过程在实践中表现得很好，但有时很难使用这些方法获得精确的最坏情况复杂度结果，特别是对于EXPTIME完全逻辑。相比之下，基于自动机的方法通常产生的算法，最佳的最坏情况下的复杂性可以很容易地证明。然而，这种方法得到的算法通常不仅是最坏情况，而且是最好情况的指数：它们首先构造一个在输入大小上总是指数的自动机，然后对这个大型自动机应用（多项式）空性测试。为了克服这个问题，必须尝试在执行空性测试的同时“动态”构建自动机。在本文中，我们将表明，模态逻辑K的Voronkov逆方法可以被看作是由K的自动机方法完成的空性测试的即时实现。这一结果的好处是双重的。首先，它表明，Voronkov的实现的逆方法，这在实践中表现得很好，是一个优化的基于自动机的可满足性过程的飞行实现K。第二，它可以用来给一个简单的证明的事实，Voronkov的优化不破坏完整的过程。我们还将表明，逆方法可以很容易地扩展到处理全球公理，并且在这种设置下，自动机方法的对应关系仍然成立。特别是，逆方法产生一个EXPTIME算法满足K w.r.t.全局公理
2004-12-22 cs.LO
