10
votes
1answer
489 views

Where can I find Gonthier's Coq code proving the four color theorem?

In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq: Gonthier, Georges. Formal proof—the four-color theorem. Notices Amer. ...
1
vote
0answers
122 views

Basis of periodic tiling of Wang tile

Given a set of Wang tile, Given 3 periodic tiling: A, B, C We define 3 vector F[A], F[B], F[C] each vector correspond to the appearing frequency of each type of tiles in the tiling. Now, we ...
2
votes
1answer
90 views

simple cycle analog in 2D (with application in tiling)

We know that any closed cycle of a graph could be decomposed into sum of simple cycles. To translate this theorem into tiling of 1D (Wang tile). We know that any 1D periodic tiling could be ...
2
votes
0answers
103 views

Graph theoretical representation of Wang Tile

We note that for one dimensional tiling problem of Wang Tile could be represented by a graph. Each cycle on the graph represents a periodic solution. However, is there a well established counter-part ...
-2
votes
1answer
185 views

Natural constructions (not depending on parameters) [closed]

Consider graph clusterings as a prototypical example of (logical) constructions. Let a clustering of a graph $(V,E)$ be any covering of $V$, i.e. a set $C$ with $\bigcup C = V$. I am looking for a ...
1
vote
0answers
149 views

Self-modelling structures

Consider - for the sake of simplicity - only graphs as structures. For undirected graphs $(V, E\subseteq \binom{V}{2})$ let $E(v)$ be the set of edges $e\in E$ incident with $v$, i.e. $\lbrace e ...
8
votes
1answer
381 views

Weakest choice principle required for Robertson-Seymour Graph Minor Theorem?

The main Robertson-Seymour Theorem states that finite graphs form a well-quasi-ordering under the graph minor relation. In other words, in every infinite set of finite graphs, there exist two graphs ...
7
votes
2answers
419 views

Deriving Konig's Lemma directly from Infinite Ramsey's Theorem for triples

Let KL denote König's Lemma (for trees over $\mathbb{N}$), and RT(3) denote the Infinite Ramsey Theorem for triples over $\mathbb{N}$ (notation as in Simpson's book Subsystems of second order ...
2
votes
1answer
196 views

Definability in a language with a single binary predicate

Let the first-order language ${\mathcal{L}}$ have a single binary predicate $P$. Consider the structure whose underlying set is ${\mathbb{Z}}$, the integers, and an ordered pair $(m,n)$ is in $P$ if ...
10
votes
4answers
1k views

How are Modal Logic and Graph Theory related?

I am currently taking a graduate logic course on Modal Logic and I can't help notice that there are a certain class of graphs characterized by the modal axioms such as (4) $\Box p \rightarrow \Box ...
2
votes
1answer
327 views

Algorithm for satisfiability of inequalities.

I am looking for an algorithm for checking the satisfiability (with natural values) of a set of inequalities made of variables and natural numbers, for example: $u < v, u \leq z, 3 \leq v$. In ...
2
votes
1answer
468 views

Composite finite-state machines

A finite state machine, FSM, is a box with C input/output channels, and S states, and a fixed map $f : S\times C \to S\times C\cup {0}$. If a state $(c_i,s_j)$ is mapped to the 0 element it means it ...
3
votes
1answer
401 views

Examples of Graphs with Trivial Definable Closure

If I'm giving a lecture on trivial definable closure (as a property of graphs), what is a good example of a graph that I can easily draw to depict the concept of trivial dcl?
5
votes
1answer
522 views

Characterization of infinite paths in graphs

First an introduction. A directed graph we all know what is, and a graph is serial whenever every vertex has a successor. I do not consider the empty graph. A pair $(\mathcal{G},s)$ is called a ...
6
votes
4answers
653 views

Self-defining structures

The relations $R$ in abstract graphs (with genuinely propertyless vertices) cannot be defined because there is nothing the relations can base on: they have to be presupposed. But consider derived ...
2
votes
3answers
399 views

Graph properties: definability and decidability

[This is a side question to Supervenience in mathematics.] There are graph properties that are not FO-definable, but MSO-, TC-, or LFP-definable. There may be other graph properties that are not ...
7
votes
3answers
478 views

Statistics for Second order properties of Random graphs

Hi! Let G(N) be the number of graphs with vertices {1, 2, ..., N} and GN(F) be the number of those of them which satisfy graph property F. There is a beautiful result by Glebskii and Fagin that limit ...
14
votes
1answer
567 views

Which graphs are elementarily equivalent to their own disjoint sums?

In Stefan Geschke's recent question, one of the solutions observed that the graph consisting of a single infinite beaded chain, a $\mathbb{Z}$-chain where each integer is connected to its nearest ...
2
votes
1answer
240 views

Graph properties and infinite FOL sentences

This question is related to this Question. Above questions revealed that even though FOL is not expressive enough to describe properties such as Connectivity, Bipartite etc. It is possible to ...
10
votes
3answers
1k views

Is non-connectedness of graphs first order axiomatizable?

A recent question asked for graph properties that are first order axiomatizable but not finitely axiomatizable. Connectedness was mentioned in the context. Connectedness can be axiomatized in ...
2
votes
5answers
739 views

Monadic Second Order (MSO) logic on graphs

Given a conflict graph $G = (V, E)$, a man has to transport a set $V$ of items/vertices across the river. Two items are connected by an edge in $E$, if they are conflicting and thus cannot be left ...
7
votes
3answers
312 views

What are other theories of causality besides graphical models and Bayesian networks?

I am trying to find some data structures/mathemetical theories to represent causal relationships which differ from graphical models or Bayesian Networks. Any ideas?
23
votes
9answers
2k views

How many groups of size at most n are there? What is the asymptotic growth rate? And what of rings, fields, graphs, partial orders, etc.?

Question. How many (isomorphism types of) finite groups of size at most n are there? What is the asymptotic growth rate? And the same question for rings, fields, graphs, partial orders, etc. ...
6
votes
1answer
663 views

An ubiquitous pattern of questions

There is an ubiquitous pattern of questions concerning assumedly any kind of mathematical object or structure: groups, graphs, numbers, categories, and so on. It goes like this (informally): Can a ...
38
votes
5answers
4k views

Which graphs are Cayley graphs?

Every group presentation determines the corresponding Cayley graph, which has a node for each group element, and arrows labeled with the generators to get from one group element to another. My main ...
3
votes
3answers
217 views

Name for “lower/upper bounds” of arbitrary relations?

Given a partial order $R_{\leq}$ over a set $D$, the set of upper bounds under $R$ of a subset $S$ of $D$ is commonly defined as $\{ y \in D | \ \forall x\in S, x R y \}$. (The set of lower bounds of ...