- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

sav08:graphs_as_interpretations [2008/03/23 13:50] maysam English Grammer |
sav08:graphs_as_interpretations [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 8: | Line 8: | ||

**No self-loops:** | **No self-loops:** | ||

- | \[ | + | \begin{equation*} |

\forall x.\ \lnot edge(x,x) | \forall x.\ \lnot edge(x,x) | ||

- | \] | + | \end{equation*} |

**Undirected graph:** | **Undirected graph:** | ||

- | \[ | + | \begin{equation*} |

\forall x.\ edge(x,y) \rightarrow edge(y,x) | \forall x.\ edge(x,y) \rightarrow edge(y,x) | ||

- | \] | + | \end{equation*} |

**Tournament:** | **Tournament:** | ||

- | \[ | + | \begin{equation*} |

- | \forall x, y.\ (edge(x,y) \lor edge(y,x)) \land \lnot (edge(x,y) \land edge(y,x)) | + | (\forall x, y.\ x \neq y \rightarrow (edge(x,y) \lor edge(y,x)) \land \lnot (edge(x,y) \land edge(y,x))) \land (\forall x. \lnot edge(x,x)) |

- | \] | + | \end{equation*} |

Note: there is no formula $F$ in this language ${\cal L} = \{edge\}$ that characterizes property "graph has no cycles". All properties expressed in first-order logic on graphs are "local". Intuitively, formula with $k$ universal quantifiers says that if we pick any set of $k$ vertices in the graph, then they (and their close neighbors) can induce only one of the finitely many specified subgraphs. | Note: there is no formula $F$ in this language ${\cal L} = \{edge\}$ that characterizes property "graph has no cycles". All properties expressed in first-order logic on graphs are "local". Intuitively, formula with $k$ universal quantifiers says that if we pick any set of $k$ vertices in the graph, then they (and their close neighbors) can induce only one of the finitely many specified subgraphs. |