论依赖原子的简洁性
计算机科学中的逻辑
2023-06-22 v3
摘要
命题组逻辑是于一阶组逻辑命题层面的类比。依赖、独立、包含、排斥与匿名等非经典原子均可于其中表达，但除依赖外所有原子仅知有指数级翻译。本文系统性比较它们在存在片段(其中分裂析取仅正出现)与具无限制否定的完整命题组逻辑中的简洁性。通过将称为公式大小博弈的Ehrenfeucht-Fraïssé博弈变体引入组逻辑，我们得到存在片段中所有原子的指数级下界。在完整片段中，我们给出所有原子的多项式级上界。
引用
@article{arxiv.1903.02344,
title = {On the Succinctness of Atoms of Dependency},
author = {Martin Lück and Miikka Vilander},
journal= {arXiv preprint arXiv:1903.02344},
year = {2023}
}