paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Embedded Finite Models beyond Restricted Quantifier Collapse

超越受限量词坍缩的嵌入式有限模型
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 2/10 · 论文属于嵌入式有限模型论与量词坍缩的纯逻辑理论研究,与用户当前关注的 LLM/Agent 用于静态分析与形式化验证、浮点程序分析、贝叶斯程序分析均无直接交集;仅在最抽象的“可判定理论/形式化验证基础”层面可能对 PL 理论有间接参考价值。引用 2 inbox
Michael Benedikt, Ehud Hrushovski
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:重新审视嵌入式有限模型理论,扩展量词坍缩分析并比较签名与可判定理论。

本文重新审视嵌入式有限模型理论中的公式求值问题:公式同时包含被约束为有限的无解释关系以及无限域上的解释词汇。传统“坍缩”结果指可把无限域上的一阶量化消去,转化为有限结构上的量化。作者研究坍缩的若干弱化:一是允许对有限结构进行高阶量化,二是允许对理论作扩张;并给出了一元签名与一般签名下坍缩性质的比较,以及对若干自然可判定理论中坍缩现象的新分析。结果为在混合有限/无限域逻辑中判定与量化消去提供了更一般的框架。

问题
如何评估同时含有限无解释关系和无限域解释词汇的逻辑公式,并刻画何时可消去无限域量化(坍缩)。
方法
在嵌入式有限模型理论框架下,通过模型论分析研究坍缩的弱化形式——有限结构上的高阶量化与理论扩张——并比较一元与一般签名、分析自然可判定理论。
评估
以数学证明与可判定性分析给出理论结果:签名间坍缩性质比较及可判定理论的新分析;无实验评估。
原文摘要(Abstract)

We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as interpreted vocabulary over an infinite domain: denoted in the past as embedded finite model theory. We extend the analysis of "collapse results": the ability to eliminate first-order quantifiers over the infinite domain in favor of quantification over the finite structure. We investigate several weakenings of collapse, one allowing higher-order quantification over the finite structure, another allowing expansion of the theory. We also provide results comparing collapse for unary signatures with general signatures, and new analyses of collapse for natural decidable theories.

链接与引用

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

BibTeX
@inproceedings{abs-2304-09231,
  title = {Embedded Finite Models beyond Restricted Quantifier Collapse},
  author = {Michael Benedikt and Ehud Hrushovski},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175804}
}