paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Hydra Battles and AC Termination

Hydra 之战与 AC 终止性
LMCS vol.Volume 21, Issue 22025匹配度 1/10 · 论文研究带 AC 符号的重写系统终止性证明，属于定理证明/重写理论，与用户关注的 LLM/Agent 改进静态分析与形式化验证、浮点程序分析、贝叶斯程序分析均无直接交集。引用 1 inbox
Nao Hirokawa, Aart Middeldorp
定理证明与证明工程
crossref: 2026-09-10

AI 速览

一句话：用带 AC 符号的重写系统忠实编码 Hercules 与 Hydra 之战，并证明其终止性。

本文研究 Hercules 与 Hydra 之战的项重写编码及其终止性证明。已有项重写编码无法忠实建模 Hercules 采取的任意战斗策略。作者将博弈编码为带 AC 符号的重写系统，使 Hercules 的任意策略都能被准确表示。为证明该编码终止，论文采用类型引入（type introduction），并结合用于 AC 重写的多排序语义标注，以及新提出的 AC-MPO——一种与 AC 兼容的归约序，可视为 AC-RPO 的大幅弱化版本。论文给出编码终止性的形式化证明，表明这些方法可用于分析此类复杂重写系统。评估以理论证明为主，摘要未提及实现或实验。

问题
如何为 Hercules 与 Hydra 之战给出忠实建模 Hercules 任意策略的项重写编码，并证明该编码终止。
方法
采用带 AC 符号的重写系统编码博弈；终止性证明结合 type introduction、多排序语义标注，并提出与 AC 兼容的新归约序 AC-MPO（AC-RPO 的弱化版本）。
评估
通过形式化证明论证编码的忠实性和终止性；摘要未提及实现或实验评估。
原文摘要（Abstract）

We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-MPO, a new AC compatible reduction order that can be seen as a much weakened version of AC-RPO.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{HirokawaM25,
  title = {Hydra Battles and AC Termination},
  author = {Nao Hirokawa and Aart Middeldorp},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 2},
  year = {2025},
  doi = {10.46298/lmcs-21(2:29)2025}
}