Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+
我们开发了一个健全的，完整的，实际上可实现的基于表格的决策方法建设性的可满足性测试和模型合成的片段ATL+的完整交替时间时序逻辑ATL*。该方法扩展了一个基本的方式以前开发的基于表格的ATL的决策方法和工程在2EXPTIME，这是最佳的最坏情况下的可满足性问题的ATL+的复杂性。我们还讨论了如何适当的参数化和语法限制输入ATL+公式类可以降低可满足性问题的复杂性。
2015-05-27 cs.LO
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
本文是一个贡献的理论基础和有效的自动化证明程序的非经典逻辑的实际建设。我们在这里集中在有限值逻辑的情况下，并展示：（i）一种机制，用于产生一个类似经典的描述，他们在一个有效的各种二价语义;（ii）用于从如此获得的二价语义中提取均匀（classically-labeled）cut-免费的标准分析表格与可能的分支可逆规则，并与证明策略配对，旨在保证终止的相关的证明程序;（iii）一种机制，也提供了相同的逻辑，统一的削减为基础的表系统与线性规则。后者的表系统被证明是足够的，即使限制到分析削减，他们也被证明多项式模拟真值表，一个功能，是不享有的前标准类型的表系统（甚至在2值的情况下）。结果是基于有用的概括的概念的分析性和组合性，并说明了一个理论，适用于许多其他类别的非经典逻辑。
2014-08-16 cs.LO
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
Certification of Prefixed Tableau Proofs for Modal Logic
不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑
2016-09-14 cs.LO
A tableau for set-satisfiability for extended fuzzy logic BL
本文给出了一种表演算，用于求扩展的模糊逻辑BL、具有附加Baaz联结子和对合否定的模糊逻辑BL的公式的集合可满足有限集的模型，如果这样的模型存在的话。该演算是BL的Tableau演算的推广，它基于连续t-范数的分解定理。上述BL的表演算用于证明扩展BL的公式A对于所有连续t-范数是有效的，或者用于找到连续t-范数 * 和命题原子到[0，1]的赋值V，使得 *-求值V*（A）<1。本文提出的表演算使得对于扩展BL的有限公式集F和[0，1]的子集K，可以找到一个连续的t-范数 * 和命题原子到[0，1]的赋值V，使得对于所有属于F的公式A，*-求值V*（A）属于K，或者证明这样的模型不存在。
2014-07-11 cs.LO
Non-Analytic Tableaux for Chellas's Conditional Logic CK and Lewis's Logic of Counterfactuals VC
Priest为Chellas的条件逻辑Ck提供了一个简单的tableau演算。我们提供的规则，当添加到牧师的系统，结果在画面演算切拉斯的CK和刘易斯的VC。然而，这些场景的完整性依赖于截规则。
2018-05-23 cs.LO math.LO
A traditional tree-style tableau for LTL
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。我们提出了一个新的简单的传统风格的树形画面LTL，并证明它是健全的和完整的。除了易于理解，向学生介绍和手动使用外，它似乎也易于实现，并有望在自动化方面具有竞争力。它特别适合于并行实现。
2016-04-13 cs.LO
Data-Aware Hybrid Tableaux
Universidad Nacional de Córdoba（科尔多瓦国立大学）；Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET)（国家科学研究委员会）；Universidad Nacional de Río Cuarto（里奥夸尔托国立大学）
本文提出了一种用于XPath的数据感知混合表aux演算，证明其正确性、完整性和终止性，并展示了其在多项式空间内的探索能力，确立了该逻辑的可满足性问题为P空间完全。
2025-12-04 cs.LO
A New Rule for LTL Tableaux
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。在本文中，我们介绍了一种新的风格的tableau规则，支持一个新的简单的传统风格的树形tableau LTL。我们证明它是健全和完整的。除了易于理解，向学生介绍和使用外，它还易于实现，并且与最先进的系统相比具有竞争力。它特别适合于并行实现。
2016-09-14 cs.LO
Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning
我们提出了一些逻辑的非单调推理，由克劳斯，莱曼和Magidor定义的表演算。我们给出了所有KLM逻辑，即优先，循环累积，累积和理性逻辑的一个Tableau证明过程。我们的演算是通过引入合适的模态来解释条件断言而获得的。我们提供了一个决策程序的逻辑考虑，我们研究它们的复杂性。
2006-11-10 cs.AI cs.LO
Tableau Proof Systems for Justification Logics
本研究针对多种证明逻辑构建Tableau证明系统，证明其相对于Mkrtychev模型的可靠性与完备性，通过句法证明实现切消以支撑完备性，还验证了系统的子公式性质，为证明逻辑的推理研究提供了形式化工具。
2016-04-11 cs.LO math.LO
Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics
本文提出二元混合逻辑的完备表记演算，同时构建了依赖维度的混合依赖积逻辑演算，并证明其完备性，但所有系统均不具终止性。
2023-11-14 cs.LO math.LO
Tableau methodology for propositional logics
Monash University, Melbourne, Australia（莫纳什大学）
本文提出了一种通用的表格法方法，用于生成命题逻辑的表格系统，并推广了Smullyan和Fitting的抽象一致性属性。
2025-11-20 cs.LO math.LO
ExpTime Tableaux with Global Caching for Hybrid PDL
提出了混合命题动态逻辑的第一个具有ExpTime复杂度的直接表决策过程。它检查HPDL中给定的ABox（断言的有限集合）是否可满足。从技术上讲，它将全局缓存与检查可能性的实现和处理名词相结合。我们的过程包含了足够的细节，可以直接实现，并且已经在TGC2（具有全局缓存的表）系统中实现。由于HPDL可以作为一个描述逻辑来表示和推理术语知识，我们的过程是有用的实际应用。
2017-05-02 cs.LO
STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
IMT Lucca（卢卡高等研究学院）；TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
研究针对网络物理系统中STL公式一致性检查难题，指出原表格法缺陷，提出新树形表格法并证明其可靠性与完备性，基于此开发STLSat工具，能判定可满足性等，评估显示其性能优于现有工具。
2026-09-18 cs.LO
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Politecnico di Milano（米兰理工大学）；TU Wien（维也纳工业大学）
针对信息物理系统中带界时间算子的离散时间信号时序逻辑（STL）的可满足性检验需求，提出一种利用时间区间冗余加速的树形单次表算法，可拓展用于多种STL相关验证任务，性能优于现有最优编码方法。
2025-07-29 cs.LO
One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past
在本文中，我们提出了一个新的一遍和树形tableau方法的时间命题时态逻辑和有界的变体与过去的运营商的扩展。时间命题时态逻辑（TPTL）是一种具有EXPSPACE完全可满足性问题的实时时态逻辑，已成功地应用于实时系统的验证。与LTL相反，将过去运算符添加到TPTL使得结果逻辑（TPTL+P）的可满足性问题非初等。在本文中，我们设计了一个一遍和树形tableau的TPTL和有界TPTL+P（TPTLb+P），一个语法限制引入编码的时间线为基础的规划问题，恢复EXPSPACE完全的复杂性。TPTL和TPTLb+P的tableau系统以统一的方式呈现，彼此非常相似，提供了一个通用的骨架，然后专门用于每个逻辑。在此过程中，我们将TPTLb+P的语义转换为TPTL+P的一个纯句法片段，给出了一个将前者嵌入后者的翻译。充分证明了系统的可靠性和完备性。特别是，我们给出了一个大大简化的模型理论的完备性证明，它回避了复杂的组合参数所使用的已知证明的一遍和树形tableau系统的LTL和LTL+ P。
2018-09-10 cs.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
An optimized KE-tableau-based system for reasoning in the description logic $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$ (Extended Version)
本文提出优化的KE$^γ$-tableau系统，用于描述逻辑$\mathcal{DL}_{\mathbf{D}}^{4,\\!\times}$的TBox和ABox推理，实验表明其性能比现有系统提升约400%。
2024-02-20 cs.LO
Tableaux for the Logic of Strategically Knowing How
Nankai University（南开大学）；College of Philosophy, Nankai University（南开大学哲学院）
本文为多智能体策略性知道如何逻辑提出了表推演过程，证明了其可靠性与完备性，并证明该逻辑的可满足性问题可在 PSPACE 内判定。
2023-07-11 cs.AI cs.LO
Tableau-based procedure for deciding satisfiability in the full coalitional multiagent epistemic logic
我们研究了多智能体认知逻辑CMAELCD与运营商的共同和分布式知识的所有联盟的代理。我们引入Hintikka结构的逻辑，并证明了在这样的结构中的可满足性是等同于在标准模型中的可满足性。利用这一结果，我们设计了一个增量式的基于表的决策过程中测试CMAELCD的可满足性。
2009-02-12 cs.LO cs.MA
Tableau-based decision procedure for non-Fregean logic of sentential identity
带恒等式的句子演算（SCI）是经典命题逻辑的一种扩展，其特点是在公式之间增加了一种新的恒等式连接符。在SCI中，如果两个公式具有相同的符号，则称它们相同。在逻辑的语义学中，真值与指称是不同的，因此恒等连接词严格强于经典等价。在本文中，我们提出了一个健全的，完整的，并终止算法决定可满足性的SCI公式，基于标记表。据我们所知，这是第一个在NP中运行的SCI决策过程，即，是复杂性最优的。所获得的复杂性界是一个结果，在算法中的推导规则分为两组：分解和平等的规则，其相互作用产生推导树的分支多项式长度相对于调查公式的大小。我们描述了一个实现的过程，并比较其性能与其他结石的SCI（然而，终止结果没有建立）的实现。我们展示了我们的算法可能的改进，并讨论了将其扩展到其他非Fregean逻辑的可能性。
2021-04-29 cs.LO
Automated Synthesis of Tableau Calculi
本文提出了一种合成声音和完整画面的方法。给定逻辑的形式语义的规范，该方法生成一组可用于在逻辑内推理的tableau推理规则。该方法保证生成的规则形成一个演算，这是健全的和建设性的完整。如果逻辑可以被证明允许有限过滤相对于一个定义良好的一阶语义，然后添加一个通用的阻塞机制提供了一个终止表演算。生成tableau规则的过程可以完全自动化，并且与阻塞机制一起产生用于生成tableau决策过程的自动化过程。为了说明，我们显示的描述逻辑与传递角色和命题直觉逻辑的方法的可行性。
2012-04-23 cs.LO cs.SC
Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time
我们开发了一个基于表格的决策过程的充分联盟的多智能体的时间认知逻辑的线性时间CMATEL（CD+LT）。它扩展了LTL与运营商的共同和分布式知识的所有联盟的代理。Tableau程序以指数时间运行，与Halpern和Vardi为我们的逻辑片段获得的下限相匹配，从而为CMATEL（CD+LT）提供了一个复杂性最优的决策程序。
2019-11-21 cs.LO cs.MA
An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More
最近，作者提出了下近似逻辑推理的程序。到目前为止，所有这些逻辑都局限于对单个程序行为的推理。然而，存在许多过度近似的关系逻辑，用于对程序对进行推理并将其行为关联起来。我们提出了第一个下近似关系逻辑，简单的命令式语言IMP。我们证明了我们的逻辑是健全的和完整的。此外，我们展示了如何在这个逻辑推理可以分解成非关系推理下近似霍尔逻辑，反映Beringer的结果过近似的关系逻辑。我们说明了我们的逻辑在一些小的例子中，我们证明了不安全的存在。
2020-03-11 cs.LO
A Parallel Linear Temporal Logic Tableau
对于许多应用程序，我们无法充分利用超级计算机或云计算提供的潜在大规模并行化，因为很难解决如何以这种方式在处理器之间分配计算任务以最小化通信需求。然而，最近开发的分支独立tableaux的共同LTL时序逻辑应该直观地容易并行化，因为每个分支可以独立开发。在这里，我们描述了一种简单的技术，用于划分这样的表，使每个分区可以独立处理，而不需要进程间通信。我们调查在何种程度上，这种技术提高了标准的基准和随机公式的LTL表的性能。
2017-09-07 cs.LO cs.PF
Complete and Terminating Tableau Calculus for Undirected Graph
本文针对无向图构造混合逻辑的表列方法，证明其完备性与终止性，并由此得出该逻辑的可判定性。
2024-11-25 cs.LO math.LO
The relational model is injective for Multiplicative Exponential Linear Logic
本文证明了乘性指数线性逻辑（MELL）的一个完备性结果：证明了关系模型对于MELL证明网是单射的，即关系模型中MELL证明网之间的相等性是用割消法精确公理化的。
2016-05-10 cs.LO
Tableau-based decision procedures for logics of strategic ability in multi-agent systems
University of the Witwatersrand（威特沃特斯兰德大学）
我们开发了一个增量的基于表的决策过程的交替时间时序逻辑ATL和它的一些变种。虽然在理论上建立的复杂性上限内运行，我们声称，我们的画面实际上是更有效的平均情况下，比其他决策程序ATL已知的。此外，其适应ATL的变体的容易性证明了所提出的程序的灵活性。
2008-09-09 cs.AI cs.LO cs.MA
Terminating Calculi for Propositional Dummett Logic with Subformula Property
本文给出了两个满足子公式性质的命题Dummett逻辑的终止表演算。我们演算的思想依赖于Dummett逻辑的线性有序Kripke语义。第一个演算在两个语义层面上工作：现在和下一个可能世界。第二个演算采用通常的对象语言的Tableau系统，并利用一个属性的建设的完整性定理，引入一个检查，这是一种替代循环检查机制。
2012-06-20 cs.LO
Approximate Relational Hoare Logic for Continuous Random Samplings
近似关系霍尔逻辑（Approximate Relational Hoare Logic，简称apRHL）是一种用程序设计语言pWHILE编写的用于数据库差分隐私的形式化验证的逻辑。然而，严格地说，这种逻辑只处理离散的随机采样。本文定义了Giry monad亚概率变体的分级关系提升，它描述了差分隐私。我们扩展的逻辑apRHL与此分级提升处理连续随机采样。本文给出了连续随机抽样情形下apRHL证明规则的一般方法。
2016-03-04 cs.LO
Evidence Logics with Relational Evidence
动态证据逻辑是在动态环境中对代理的证据和基于证据的信念进行推理的逻辑。在本文中，我们介绍了一个家庭的逻辑推理的关系证据：证据，涉及一个排序的国家在其相对的可扩展性。我们提供了健全的和完整的公理化的逻辑。我们还提出了几个证据行动，并证明了相关的动态逻辑的可靠性和完备性。
2017-06-19 cs.LO
Local Variables and Quantum Relational Hoare Logic
我们将局部变量添加到量子关系霍尔逻辑（Unruh，POPL 2019）。我们推导出支持局部变量的推理规则（包括改进的“对手规则”）。我们扩展了qRHL的计算机辅助验证的qrhl工具，以支持本地变量和我们新的推理规则。
2020-07-28 cs.LO
Relational Parametricity and Separation Logic
分离逻辑是霍尔逻辑的一个新的扩展，用于推理引用共享可变数据结构的程序。在本文中，我们提供了一个新的解释逻辑的程序设计语言具有更高的类型。我们的解释是基于雷诺的关系参数化，它提供了一个正式的连接之间的分离逻辑和数据抽象。
2008-05-15 cs.LO
Complexity through Translations for Modal Logic with Recursion
本文研究了经典模态逻辑的复杂性及其扩展与不动点算子，使用翻译转移结果跨越逻辑。特别是，我们通过翻译和从μ演算和模态逻辑，这使我们能够转移已知的上限和下限的多智能体逻辑的复杂性结果。我们还使用这些翻译介绍一个终止表系统的逻辑，我们研究的基础上，Kozen的表的μ演算，和一个拟合和Massacci模态逻辑。
2022-09-21 cs.LO
Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies
在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。
2013-12-10 cs.LO math.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
Verifying Relational Properties using Trace Logic
我们提出了一个逻辑框架，在命令式程序中的关系属性的验证。我们的工作是出于安全应用程序的关系属性，往往需要推理公式与量词交替。我们的框架减少了验证的关系属性的命令式程序的有效性问题到跟踪逻辑，一阶谓词逻辑的表达实例。跟踪逻辑从它的语法中提取它的表达能力，这允许在计算跟踪上表达属性。它的公理化支持程序执行中中间步骤的细粒度推理，特别是循环迭代。我们提出了一个算法来编码的语义程序，以及它们的关系属性的跟踪逻辑，然后显示如何一阶定理证明可以用来推理所产生的跟踪逻辑公式。我们的工作是在快速工具中实现的，并与来自安全领域的例子进行评估。
2019-08-12 cs.LO
A tableau methodology for deontic conditional logics
在本文中，我们提出了一个定理证明方法的限制，但重要的片段的条件语言（布尔组合）条件语句与非嵌套的前件。该方法基于条件逻辑的可能世界语义。KEM标签形式主义，旨在说明正常模态逻辑的语义，很容易适应条件逻辑的语义，通过简单的索引标签与公式。推理规则由命题系统KE+提供-一个类似表格的分析证明系统，设计用于反驳和直接证明方法-扩大了条件连接词的适当消除规则。我们将要提出的定理证明方法可以被看作是为（可废止的）条件义务的几个条件逻辑开发适当的算法框架的第一步。
2000-03-10 cs.AI cs.LO
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
本文针对依赖类型高阶逻辑DHOL提出原生表推演自动推理规则，并在Lash中实现，借助DHOL到HOL的可靠完备翻译保证完备性，实验表明其性能优于在翻译结果上运行的主流HOL证明器。
2024-10-18 cs.LO
A Tableau Construction for Finite Linear-Time Temporal Logic
本文描述了一种将有限命题线性时间时态逻辑（Finite LTL）中的公式转换成有限状态自动机的方法，该自动机的语言是给定公式的模型。有限LTL与传统LTL的不同之处在于，公式是关于有限而不是无限的状态序列来解释的;这一事实意味着传统的有限状态自动机，而不是像Büchi和其他人开发的ω-自动机，足以识别这样的公式的模型。所考虑的方法是基于众所周知的表格建设技术开发的LTL，我们在这里适应有限LTL的设置。所得到的自动机可用作模型检验、可满足性测试和模型综合的基础。
2020-06-22 cs.FL cs.LO
Relational Logic with Framing and Hypotheses: Technical Report
关系属性出现在许多设置：相关的两个版本的程序，使用不同的数据表示，不干扰属性的安全性，等关系验证的主要成分，有关对齐对中间步骤，已被用于在许多伪装，但现有的关系程序逻辑的范围很窄。本文介绍了一种基于新语法的逻辑，它将产品程序编织在一起，以表达关系公式被断言的控制流点的对齐。正确性判断的特点假设与关系规范，由一个规则的链接过程的实现。该逻辑支持关于包含相似和不相似的控制和数据结构的程序对的推理。推理动态分配的对象支持的框架规则的基础上的框架条件服从SMT证明。我们证明了合理性，并勾勒出逻辑如何用于数据抽象，循环优化和安全的信息流。
2016-11-28 cs.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)
我们证明了对于乘法指数线性逻辑（无弱化），割消法所引起的证明的句法等价关系与基于多集的关系模型所引起的证明的语义等价关系一致：一个是说模型（或语义）中的解释是单射的.我们实际上证明了一个更强的结果：两个无割证明的完整的乘法和指数片段的线性逻辑，其解释一致的多集为基础的关系模型是相同的“指数盒的门之间的连接”。
2011-02-07 cs.LO
On the Relational Translation Method for Propositional Modal Logics
模态逻辑中定理证明的一种方法是将它们转换为谓词演算，然后使用传统的归结式定理证明器。这种方法在实践中被认为是不合适的，因为得到的公式太长，而且不可能证明模态公式的非定理性。在本文中，我们证明了（关系）翻译方法的实际可行性。使用最先进的一阶谓词逻辑定理证明器，我们证明了模态逻辑文献中的许多基准定理。我们证明了命题模态和时态逻辑公式的无效性，使用模型生成器或可满足性测试的经典逻辑。许多可满足的公式被发现具有非常小的模型。最后，几种不同的方法进行了比较。
2021-12-29 cs.LO
An ExpTime Procedure for Description Logic $\mathcal{ALCQI}$ (Draft)
针对$\mathcal{ALCQI}$中的可满足性问题，给出了一个基于ExpTime表的最坏情况决策过程。一般公理
2007-03-18 cs.LO
An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability
提出了一种基于表格的命题动态逻辑可满足性判定算法，该算法建立一个具有祖先循环的有限根树，并在回溯过程中将子循环的额外信息传递给父循环，以区分好循环和坏循环.它很容易实现，具有并行化的潜力，因为它通过独立地探索每个tableau分支来构建一个伪模型。但它的最坏情况行为是2EXPTIME而不是EXPTIME。TWB（http：//www.example.com）中的原型实现是可用的。twb.rsise.anu.edu.au
2008-01-08 cs.LO
Relational Dualities and Bisimulation
University of Bristol（布里斯托大学）
本文探讨了关系对偶性与双射之间的对应关系，通过构建特定的关系扩展，将良好的系统间关系（如双射）与谓词间的关系联系起来。
2026-05-07 cs.LO
A quantitative probabilistic relational Hoare logic
本文提出定量关系概率程序逻辑 eRHL，利用扩展非负实数断言突破 PRHL 与 apRHL 的随机性对齐限制，并证明其在程序等价、统计距离和差分隐私上的可靠完备性。
2025-01-08 cs.LO
Terminating Hybrid Tableaus for Ordered Models
本文提出三种终止表aux系统，用于处理严格偏序、无界严格偏序和偏序模型，通过引入名义来描述二元关系属性，提升部分序处理能力。
2026-03-16 cs.LO math.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
Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge
Roskilde University（罗斯基勒大学）；Technical University of Denmark（丹麦技术大学）；University of Johannesburg（约翰内斯堡大学）；University of the Witwatersrand（威特沃特斯兰德大学）
我们开发了一个概念清晰，直观，可行的决策程序，用于测试可满足性在充分的多智能体认知逻辑CMAEL（CD）与运营商的共同和分布式知识的语言中提到的所有联盟的代理。为此，我们引入了CMAEL（CD）的Hintikka结构，并证明了在这种结构中的可满足性等价于标准模型中的可满足性。使用该结果，我们设计了一个增量的tableau建设过程，最终构建一个令人满意的Hintikka结构的CMAEL（CD）的公式的每一个可满足的输入集，并关闭每一个不可满足的输入集的公式。
2012-01-25 cs.AI cs.LO math.LO
Alignment complete relational Hoare logics for some and all
Stevens Institute of Technology（史蒂文斯理工学院）；Dartmouth College（达特茅斯学院）
本文针对关系验证中的计算步骤对齐问题，提出并证明了针对∀∀和∀∃性质的关系型霍尔逻辑的对齐完备性，同时讨论了对齐在关系推理中的局限性并提出蕴含完备性作为评估手段。
2025-11-07 cs.LO
Relational Differential Dynamic Logic
在混合动力系统（结合连续物理动力学和离散数字控制）的质量保证领域，Platzer的微分动态逻辑（dL）被广泛认为是一种具有坚实数学基础和复杂工具支持的演绎验证方法。受我们的行业合作伙伴提供的基准测试的启发，我们研究了dL的关系扩展，旨在正式证明诸如“较早部署紧急制动器会降低碰撞速度”之类的陈述。“这里的一个主要技术挑战是将两种动态在不同时间点的两种状态联系起来。我们的主要贡献是合适的模拟理论（微分不变量的关系扩展，是中心的证明方法在dL），和时间拉伸的派生技术。后者具有特别高的适用性，因为用户不必从空气中合成模拟。我们从这些概念中推导出新的dL推理规则，并通过几个汽车案例研究证明了它们的使用。
2020-03-12 cs.LO
