A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
A Polynomial Translation from the Two-Variable Guarded Fragment with Number Restrictions to the Guarded Fragment
复制标题
从带数量限制的二变量保护片段到保护片段的多项式翻译
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Yevgeny Kazakov
中科院分区：
文献类型：
--
作者：
Yevgeny Kazakov
本文考虑二元关系的一个二元带数目限制的保护片段，并给出该片段中公式到三元保护片段的一个保满足性变换。翻译可以在多项式时间内计算，并产生一个公式，该公式在初始公式的大小上是线性的，即使对于数字限制的二进制编码也是如此。这使得人们可以减少推理问题的许多描述逻辑的可满足性问题的保护片段。
We consider a two-variable guarded fragment with number restrictions for binary relations and give a satisfiability preserving transformation of formulas in this fragment to the three-variable guarded fragment. The translation can be computed in polynomial time and produces a formula that is linear in the size of the initial formula even for the binary coding of number restrictions. This allows one to reduce reasoning problems for many description logics to the satisfiability problem for the guarded fragment.