paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Axiomatizations and Computability of Weighted Monadic Second-Order Logic

加权一元二阶逻辑的公理化与可计算性
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10 · 论文研究加权一元二阶逻辑的公理化与可判定性,属于逻辑与自动机理论基础,与用户关注的静态分析、LLM/Agent、浮点或贝叶斯程序分析没有直接交集;仅与形式化验证/形式语义有非常间接的联系。引用 0 inbox
Antonis Achilleos, Mathias Ruggaard Pedersen
crossref: 2026-09-12

AI 速览

一句话:为加权一元二阶逻辑及其无一般和片段给出完备公理化,并分析相关判定问题的可判定性与不可判定性。

加权一元二阶逻辑是能精确刻画加权自动机行为的逻辑,其语义相对于半环参数化。Gastin 与 Monmege(2018)曾给出该逻辑一种版本的抽象语义,以获得其与加权自动机等价性的更一般且模块化的证明。本文聚焦该抽象语义,分别为完整逻辑和去掉一般和的片段建立完备公理化,从而更细粒度地理解该逻辑。文章还讨论经典逻辑语言判定问题如何适配到加权设定,并证明其中许多问题可判定,但会继承底层一阶与二阶逻辑的较差复杂度;同时证明在采用抽象解释时,加权可满足性是不可判定的。

问题
如何在加权一元二阶逻辑的抽象语义下,为完整逻辑及关键片段建立完备公理化,并理解其判定问题的可计算性。
方法
在 Gastin 与 Monmege 的抽象语义框架中,分别为完整逻辑和无一般和的片段构造完备公理系统,并将经典逻辑判定问题适配到加权设定。
评估
通过数学证明给出公理化的完备性,并分析多个判定问题的可判定性与复杂度;进一步证明抽象解释下的加权可满足性不可判定。
原文摘要(Abstract)

Weighted monadic second-order logic is a weighted extension of monadic second-order logic that captures exactly the behaviour of weighted automata. Its semantics is parameterized with respect to a semiring on which the values that weighted formulas output are evaluated. Gastin and Monmege (2018) gave abstract semantics for a version of weighted monadic second-order logic to give a more general and modular proof of the equivalence of the logic with weighted automata. We focus on the abstract semantics of the logic and we give a complete axiomatization both for the full logic and for a fragment without general sum, thus giving a more fine-grained understanding of the logic. We discuss how common decision problems for logical languages can be adapted to the weighted setting, and show that many of these are decidable, though they inherit bad complexity from the underlying first- and second-order logics. However, we show that a weighted adaptation of satisfiability is undecidable for the logic when one uses the abstract interpretation.

链接与引用

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

BibTeX
@inproceedings{paperbot6244,
  title = {Axiomatizations and Computability of Weighted Monadic Second-Order Logic},
  author = {Antonis Achilleos and Mathias Ruggaard Pedersen},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470615}
}