带计数的 MTL 的表达能力
计算机科学中的逻辑
2012-09-05 v1
摘要
众所周知，具有整数端点的 MTL 无法表达序与度量的所有一元一阶逻辑 (FO(<,+1))。事实上，MTL 无法表达计数模态算子 ，该算子断言某性质在下一个时间区间内成立 次。我们证明，带有计数模态算子的 MTL（即 MTL+C）对于 FO(<,+1) 是表达完备的。这一结果有力地支持了 Hirshfeld 和 Rabinovich 的论断，即 Q2MLO 是 FO(<,+1) 最具表达能力的可判定片段。
引用
@article{arxiv.1209.0518,
title = {The expressiveness of MTL with counting},
author = {Paul Hunter},
journal= {arXiv preprint arXiv:1209.0518},
year = {2012}
}
备注
Preliminary version - proof notes only