Two-variable logic with counting and trees
W Charatonik, P Witkowski - ACM Transactions on Computational Logic …, 2016 - dl.acm.org
ACM Transactions on Computational Logic (TOCL), 2016•dl.acm.org
We consider the two-variable logic with counting quantifiers (C2) interpreted over finite
structures that contain two forests of ranked trees. This logic is strictly more expressive than
standard C2 and it is no longer a fragment of first-order logic. In particular, it can express that
a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also
strictly more expressive than first-order logic with two variables and two successor relations
of two finite linear orders. We present a decision procedure for the satisfiability problem for …
structures that contain two forests of ranked trees. This logic is strictly more expressive than
standard C2 and it is no longer a fragment of first-order logic. In particular, it can express that
a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also
strictly more expressive than first-order logic with two variables and two successor relations
of two finite linear orders. We present a decision procedure for the satisfiability problem for …
We consider the two-variable logic with counting quantifiers (C2) interpreted over finite structures that contain two forests of ranked trees. This logic is strictly more expressive than standard C2 and it is no longer a fragment of first-order logic. In particular, it can express that a structure is a ranked tree, a cycle, or a connected graph of bounded degree. It is also strictly more expressive than first-order logic with two variables and two successor relations of two finite linear orders. We present a decision procedure for the satisfiability problem for this logic. The procedure runs in NExpTime, which is optimal since the satisfiability problem for plain C2 is NExpTime-complete.
ACM Digital Library以上显示的是最相近的搜索结果。 查看全部搜索结果