Algorithmic Correspondence for Hybrid Logic with Binder
Zhiguang Zhao
在本文中，我们发展的算法对应理论的混合逻辑与捆绑。我们定义了一类Sahlqvist不等式，其中每个不等式都有一个一阶框架对应的算法ALBA有效地计算。
In the present paper, we develop the algorithmic correspondence theory for hybrid logic with binder. We define the class of Sahlqvist inequalities, each inequality of which is shown to have a first-order frame correspondent effectively computable by an algorithm ALBA.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies
在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。
Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder
在本文中，我们继续在\cite{Zh21c}的研究，发展的Sahlqvist型完备性理论的混合逻辑与满意运营商和向下绑定$\mathcal{L}(@, \downarrow)$。我们按照\cite{ConRob}中的思想定义了$\mathcal{L}(@, \downarrow)$的骨架Sahlqvist公式类，但是我们遵循了一种不同的证明策略，这是纯粹的证明理论，即对于每个骨架Sahlqvist公式$ϕ$及其混合纯对应$π$，$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$证明了$π$，因此$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$相对于$π$定义的框架类是完备的，使用\cite{Zh21c}中定义的算法$\mathsf{ALBA}^{\downarrow}$的受限版本。
A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (extended version)
在以前的作品中，已经定义了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作展示了如何扩展这样的演算多模态逻辑丰富的功能主要用于描述逻辑：传递性和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。终止的存在，健全的和完整的演算所考虑的逻辑证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑不危及可判定性。在这项工作中证明的一个进一步的结果是，逻辑扩展所考虑的片段，除了分级模态（模态对应的数量限制的描述逻辑）有一个不可判定的可满足性问题，除非进一步的语法限制放置在通用分级模态。
Permissive-Nominal Logic (journal version)
本文介绍宽容名义逻辑（PNL），一种扩展一阶谓词逻辑以支持绑定器的逻辑，能有限公理化算术及带绑定的名义数据类型，兼具高阶逻辑的表达力与一阶逻辑的简洁性。
Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)
非确定性算法过程PEARL（“Propositional variables Elimination Algorithm for Relevance Logic”的首字母缩写）最近已经被开发用于根据标准的Meilley-Meyer关系语义来计算相关逻辑RL的语言的公式的一阶等价物。它成功的一大类公理的相关逻辑，包括所有所谓的归纳公式。在目前的工作中，我们从代数的角度重新解释PEARL，其重写规则被视为操纵在厄克特的相关代数上解释的准不等式，并报告其最近的Python实现。我们还证明了PEARL成功的所有公式都是规范的，即，在相关代数的典型扩张下保持不变。这推广了厄克特1996年论文中的“通过对应的正规性”结果。我们还指出，稍加修改，PEARL可以应用到集束蕴涵代数和关系代数。
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages
本文研究了框架$\langle \mathbb{N}, \leq \rangle$、$\langle \mathbb{N}, < \rangle$、$\langle \mathbb{Q}, \leq \rangle$、$\langle \mathbb{Q}, < \rangle$、$\langle \mathbb{R}, \leq \rangle$、$\langle \mathbb{R}, < \rangle$的一阶单峰逻辑以及一些相关逻辑在单个变量的数目以及谓词字母的数目和数量有限制的语言中的算法性质。我们表明，基于$\mathbb{N}$的框架的逻辑是$Π^1_1$ -硬-因此，不递归可重复-在语言中有两个单独的变量，一个一元谓词字母和一个命题字母。我们还表明，基于$\mathbb{Q}$和$\mathbb{R}$的框架的逻辑是$Σ^0_1$ -硬的语言具有相同的限制。类似的结果得到了一些相关的逻辑。
Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$
本文在 Lean 4 中完成了混合逻辑 $L(\forall)$ 的机器检查完备性证明，通过结构新鲜性和存在引理 Henkin 构造两种工具解决了新鲜名称的生成问题。
Hybrid Branching-Time Logics
混合分支时间逻辑被引入作为状态变量和向下箭头绑定器的CTL类逻辑的扩展。根据最近的工作在线性框架，只有一个单一的变量逻辑被认为是。研究了结果逻辑的表达能力和可满足性的复杂性。作为主要结果，证明了几个分支时间逻辑的混合形式的可满足性问题是2 EXPTIME-完全的。这些分支时间逻辑的范围从CTL的严格片段到CTL的扩展，可以谈论过去并表达公平性。相对于CTL的复杂性差距解释了相应的简洁性结果。为了证明这个上界，将分支时间逻辑的自动机理论方法推广到混合逻辑，证明了交替单卵石Buchi树自动机的非空性是2 EXPTIME-完全的。
A state vector algebra for algorithmic implementation of second-order logic
我们提出了一个数学框架映射到一个简单的状态向量代数的二阶逻辑关系。利用这种代数，集合论的基本定理可以用算法的方式证明，因此可以用专家系统证明。我们用简单的例子说明了代数的使用，并表明，原则上，基本集合论的所有定理都可以用初等的方法恢复。所开发的技术可用于一阶和二阶逻辑的自动定理证明。
Algorithmic properties of QK4.3 and QS4.3
本文证明了谓词模态逻辑 QK4.3 和 QS4.3 在极简语言（两个个体变元、一个一元谓词字母和一个命题字母）下不可判定。
Advances in Algorithmic Meta Theorems
本文综述了算法元定理的最新进展，重点介绍FO在遗传图类上的模型检测突破、单子稳定与单子依赖图类的组合结构理论、twinwidth宽度度量，以及介于FO与CMSO之间的新逻辑对无关顶点技术和递归理解等方法提供的统一视角。
The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
混合逻辑的可满足性问题是不可判定的。这引发了一个关于可判定和可处理片段的研究计划。在本文中，我们调查的影响，限制命题部分的语言的可判定性和可满足性问题的复杂性在任意的，传递的，总的框架，框架的基础上的等价关系。我们还考虑了不同的模态和混合算子。我们跟踪边界的可判定性，并给出了精确的复杂性，大多数片段，特别是包括否定的所有片段。对于单调片段，我们能够区分容易的情况下，从困难的情况下，这取决于允许的一组操作。
A Hybrid Dynamic Logic for Event/Data-based Systems
我们提出$\mathcal{E}^{\downarrow}$ -逻辑作为一个正式的基础规范和开发的基于事件的系统与本地数据状态。该逻辑旨在涵盖从抽象需求规范到建设性规范的广泛抽象级别。我们的逻辑使用菱形和框模态结构化的行动，从动态逻辑。原子动作是成对的$e /ψ$，其中$e$是事件，而$ψ$是状态转换谓词，捕获对事件的允许反应。为了编写递归过程结构的具体规范，我们集成（控制）混合逻辑的状态变量和绑定器。语义解释依赖于事件/数据转换系统;规范细化由模型类包含定义。对于建设性规范的介绍，我们提出了操作事件/数据规范，允许熟悉的，图形表示的状态转换图。我们表明，$\mathcal{E}^{\downarrow}$ -逻辑是强大到足以通过一个单一的$\mathcal{E}^{\downarrow}$ -句子的语义的操作规范。因此，整个开发过程可以依赖于$\mathcal{E}^{\downarrow}$ -逻辑及其语义作为公共基础。这还包括各种实现构造器，以支持事件细化和并行组合等。
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
模态公式表示Kripke框架上的一元二阶性质，但在许多重要情况下，它们具有一阶等价物。计算这样的等价物对于逻辑和计算原因都是重要的。另一方面，模态公式的规范性也很重要，因为它意味着用规范公式公理化的逻辑的框架完备性。计算一个模态公式的一阶等价等价物相当于消除二阶量词。二阶量词消去有两种算法：基于约束消解的SCAN算法和基于Ackermann建立的逻辑等价的DLS算法。在本文中，我们介绍了一种新的算法，SQEMA，计算一阶等价物（使用阿克曼引理的模态版本），而且，用于证明规范的模态公式。与SCAN和DLS不同，它直接作用于模态公式，从而避免了Skolemization和随后的unskolemization问题。我们提出的核心算法，并说明它与一些例子。然后，我们证明了它的正确性和规范的所有公式上的算法成功。我们表明，它不仅成功的所有Sahlqvist公式，但也对更大的类的归纳公式，在我们以前的论文中介绍。因此，我们开发了一种纯粹的算法方法来证明模态逻辑中的规范完备性，特别是，建立了模态逻辑中迄今为止最普遍的完备性结果之一。
Dual characterizations for finite lattices via correspondence theory for monotone modal logic
我们建立了一个正式的连接算法对应理论和某些双重表征结果有限格，类似于民族的表征层次的伪变种有限格，逐步推广有限分配格。这种形式上的联系是通过单调模态逻辑来实现的。事实上，我们适应的对应算法ALBA的设置单调模态逻辑，我们使用一定的对偶诱导编码的有限格作为单调邻域框架转换格项到单调模态逻辑中的公式。
First-Order Logic with Connectivity Operators
一阶逻辑（FO）可以在图上表达许多算法问题，例如独立集和支配集问题，并通过解大小进行参数化。另一方面，FO不能表达两个顶点是否连通的非常简单的算法问题。我们丰富FO与连接谓词，是专门用来表达算法图的属性，通常在参数化算法研究。通过添加原子谓词$conn_k (x, y, z_1 ,\ldots, z_k)$，如果在$z_1,\ldots,z_k$的（赋值）被删除后，$x$（的赋值）和$y$之间存在路径，则在图中保持为真，我们获得分隔符逻辑$FO + conn$。我们表明，分离器逻辑可以表示许多有趣的问题，如反馈顶点集问题和消除距离问题的一阶可定义类。然后，我们研究了分离器逻辑的局限性，并证明它不能表示平面性，特别是，不相交的路径问题。我们通过添加原子谓词$disjoint-paths_k [(x_1, y_1 ),\ldots , (x_k , y_k )]$来获得更强的不相交路径逻辑$FO + DP$，如果对于所有$1 \le i \le k$，$x_i$和$y_i$（的赋值）之间存在内部顶点不相交路径，则这些原子谓词的求值为真。不相交路径逻辑可以表示不相交路径问题、（拓扑）子包含问题、命中（拓扑）子问题等等。最后，我们比较了新逻辑与传递闭包逻辑和一元二阶逻辑的表达能力。
Algorithmic correspondence and analytic rules
本文引入算法MASSA，可从经典模态公式生成G3K的分析几何规则与无切割推导，证明其对分析归纳公式的终止性及对应性，还拓展至归纳公式与带量词模态逻辑。
Deductive Algorithmic Knowledge
算法知识的框架假设代理使用算法来计算他们明确知道的事实。在许多感兴趣的情况下，演绎系统，而不是一个特定的算法，捕获了代理用来计算他们明确知道的东西的形式推理。我们引入了一个逻辑推理的隐式和显式的知识与后者定义的演绎系统正式的逻辑理论的代理。演绎系统的高度结构化的性质导致了在任何固定的演绎系统上解释时所产生的逻辑的非常自然的公理化。逻辑的决策问题，在一个单一的代理人的存在，是NP-完全的一般，没有比命题逻辑更难。当我们确定一个在非确定多项式时间内可判定的演绎系统时，它仍然是NP完全的。这些结果以一种简单的方式扩展到多个代理。
Curved Boolean Logic: A Contextual Generalization of Propositional Logic with Algorithmic Consequences
弯曲布尔逻辑（CBL）通过引入局部真值赋值推广命题逻辑，提出上下文感知证明演算及CBL-SAT复杂度分析，提供操作算子与噪声建模，并探讨其与SAT/CSP及大语言模型稳定性的联系。
A logic-based algorithmic meta-theorem for mim-width
我们引入了一个逻辑称为距离邻域逻辑与无环性和连通性的限制（$\mathsf{A\&C~DN}$为短），扩展了存在$\mathsf{MSO_1}$与谓词查询的顶点集的邻域和验证的连通性和无环性的顶点集在各种权力的图。在[Bergougnoux and Kanté，ESA 2019; SIDMA 2021]的基础上，我们证明了当输入图与最小宽度$w$的分支分解一起给出时，每个固定$\mathsf{A\&C~DN}$公式的模型检验问题在$n^{O(w)}$时间内是可解的。几乎所有已知在多项式时间内可解的问题都可以用这个框架来表示。我们在这个列表中添加了几个自然问题，包括要求不同解决方案的问题。只要输入图的给定分支分解在$d$ -邻域等价方面具有小索引，我们的模型检验算法就有效[Bui-Xuan，Telle和Vatshelle，TCS 2013]。因此，我们统一和扩展已知的算法树的宽度，宽度和排名宽度。我们的算法有一个单指数依赖于这三个宽度的措施和渐近匹配的运行时间的最快的已知算法的几个问题。这导致了在指数时间假设（$\mathsf{ETH}$）下对于树宽度、队列宽度和秩宽度具有紧运行时间的算法;在$\mathsf{ETH}$下对于若干问题，上述对于最小宽度的运行时间也几乎是紧的。我们的结果也是紧的表达能力的逻辑：我们表明，已经轻微的扩展我们的逻辑模型检验问题的para- $\mathsf…
Computations by fly-automata beyond monadic second-order logic
我们提出了基于逻辑的方法来构建XP和FPT图算法，参数化树宽度或宽度。我们将使用上一篇文章中介绍的飞行自动机。它们使得检查不是一元二阶可表达的属性成为可能，因为它们的状态可能包括计数器，因此它们的状态集可能是无限的。我们为这些自动机配备了输出函数，以便它们可以计算与项或图相关的值。而不是新的算法结果，我们提出的工具，很容易构建某些动态规划算法结合预定义的自动机的基本功能和属性。
A Logic-based Algorithmic Meta-Theorem for Treedepth: Single Exponential FPT Time and Polynomial Space
本研究提出带无环性、连通性和团约束的邻域算子逻辑$\textsf{NEO}_2[\textsf{FRec}]+\textsf{ACK}$，给出其单指数FPT时间、多项式空间的模型检测算法，统一拓展了树深度参数下的图问题求解结果，还为CNF-SAT等新问题提供了对应复杂度算法。
Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
本文提出了一种基于低单维性的CMSO碎片，证明其在拓扑极小图类上具有固定参数可解性，扩展了逻辑元定理到拓扑极小图类。
Technical Report: Distribution Temporal Logic: Combining Correctness with Quality of Estimation
本文提出分布时间逻辑（DTL），用于描述部分可观测系统中涉及不确定性和可能性的属性，提供了一种安全的公式化方法及监控算法，并通过救援机器人应用案例验证。
A tableau methodology for deontic conditional logics
在本文中，我们提出了一个定理证明方法的限制，但重要的片段的条件语言（布尔组合）条件语句与非嵌套的前件。该方法基于条件逻辑的可能世界语义。KEM标签形式主义，旨在说明正常模态逻辑的语义，很容易适应条件逻辑的语义，通过简单的索引标签与公式。推理规则由命题系统KE+提供-一个类似表格的分析证明系统，设计用于反驳和直接证明方法-扩大了条件连接词的适当消除规则。我们将要提出的定理证明方法可以被看作是为（可废止的）条件义务的几个条件逻辑开发适当的算法框架的第一步。
PSPACE Reasoning for Graded Modal Logics
本文给出了一个判定阶化模态逻辑Gr（K_R）可满足性的PSPACE算法，它是命题模态逻辑K_R通过计数表达式的自然推广，在知识表示领域中起着重要作用。该算法采用了tableaux的方法，是第一个已知的算法，满足问题的复杂性下限。因此，我们准确地解决了问题的复杂性，并驳斥了ExpTime-hardness猜想。我们将结果推广到逻辑Gr（K_（R \cap I））上，用逆关系和可达关系的交扩充了Gr（K_R）.这建立了一种“理论基准”，所有算法方法都可以根据它来衡量。
Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2
我们提出了一种算法RTL设计的形式化验证方法，它结合了时序逻辑等价性检查和交互式定理证明。一个Verilog模块的中间模型是用Restricted Systemic C（RAC）手工编码的，RAC是一个C的原始子集，由Systemic C的整数和定点寄存器类模板扩充。该模型被设计为尽可能的抽象和紧凑，但足够忠实的RTL允许有效的等价性检查与商业工具。然后，它会自动转换为ACL 2的逻辑，从而能够根据正式的体系结构规范对正确性进行机械检查。在本文中，我们描述了RAC语言，翻译过程，以及一些技术，方便正式分析所产生的ACL2代码。
The Algorithm of Islamic Jurisprudence (Fiqh) with Validation of an Entscheidungsproblem
关于词源和方法论的算法处理的历史背景被翻译成数理逻辑和计算机科学的术语。通过对图章提出示例性问题，引入形式逻辑结构，定义逻辑查询语言。在此基础上，设计了一种用于确定Fiqh规则的遗传算法，以实现并进一步利用法治（相对于法治）完全透明，伊斯兰法的算法完全覆盖，最终提供法律安全，法律平等，和充分的法律责任。这是通过解开和恢复经典的菲克赫方法论来实现的（通常是al-Fiqh）与一阶逻辑（FOL）子集的表达能力，可持续地用可证伪的理性论证取代特设推理。结果进行了讨论，在正式条款的完整性，可判定性和复杂性的正式Fiqh系统。形式图系统的一个Entscheidungsproblem的制定和验证。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。