paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Uniformisation of Regular Relations in First-Order Logic with Two Variables

二变量一阶逻辑中正则关系的一致化
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10 · 该论文属于纯逻辑与自动机理论,研究 FO2[<] 对正则关系的一致化问题,与用户关注的静态分析、Agentic 程序、LLM 辅助形式化验证、浮点程序分析或贝叶斯程序分析均无直接关联。仅在形式化方法与逻辑基础上存在非常间接的联系。引用 0 inbox
Nathan Lhote, Vincent Michielini, Michał Skrzypczak
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:为 FO2[<] 定义的正则关系一致化问题给出判定算法,并提出该逻辑可定义语言的新表示。

本文研究有限字上正则关系的 FO2[<] 一致化问题:给定一个二元正则关系,判定其中是否存在一个与其定义域相同、且可由二变量一阶逻辑 FO2[<] 定义的单值(函数式)子关系。作者提出了一种刻画 FO2[<] 可定义语言的新表示,并基于该表示设计了判定算法,从而证明该一致化问题是可判定的。该表示还可用于解决涉及 FO2[<] 的其他问题,例如判定两个正则语言能否被某个 FO2[<] 可定义语言分离。

问题
给定有限字上的正则二元关系,判定它是否具有可由 FO2[<] 定义的一致化,即包含于原关系、定义域相同且函数式的子关系。
方法
给出 FO2[<] 可定义语言的一种新表示,并据此构造判定正则关系是否可 FO2[<] 一致化的算法。
评估
以可判定性证明为核心,并展示新表示也可用于 FO2[<] 相关问题的判定,例如两个正则语言的 FO2[<] 可分离性。
原文摘要(Abstract)

A uniformisation of a binary relation is a functional relation contained in it, with the same domain. The uniformisation problem asks whether such a uniformisation can be defined in a given formalism. We solve this problem in the context of regular relations over finite words, for the fragment FO2[<] of First-Order Logic with two variables: we provide an algorithm that decides if a given regular relation over finite words admits a uniformisation definable in FO2[<]. The paper provides a new representation of languages definable in FO2[<], which can be used for the decidability of other problems involving this formalism, e.g. the problem of separability of two regular languages by a language definable in FO2[<].

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{LhoteMS24,
  title = {Uniformisation of Regular Relations in First-Order Logic with Two Variables},
  author = {Nathan Lhote and Vincent Michielini and Michał Skrzypczak},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662114}
}