Content deleted Content added
No edit summary |
added a small section on the WL algorithm (more to come) |
||
Line 12:
The two-variable fragment of first-order logic with no function symbols is known to be decidable even with the addition of [[counting quantifiers]]<ref>E. Grädel, M. Otto and E. Rosen. ''Two-Variable Logic with Counting is Decidable.'', Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.</ref>, and thus of [[uniqueness quantification]]. This is a more powerful result, as counting quantifiers for high numerical values are not expressible in that logic.
== Connection to the Weisfeiler-Leman algorithm ==
There is a strong connection between two-variable logic and the Weisfeiler-Leman (or color refinement) algorithm. Given two graphs, then any two nodes have the same stable color in color refinement if and only if they have the same ''C^2'' type, that is, they satisfy the same formulas in two-variable logic with counting<ref>Grohe, Martin. "Finite variable logics in descriptive complexity theory." Bulletin of Symbolic Logic 4.4 (1998): 345-398.</ref?.
== References ==
| |||