# [isabelle] New AFP entry: Properties of Random Graphs -- Subgraph Containment

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Properties of Random Graphs -- Subgraph Containment
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Fri, 14 Feb 2014 08:44:14 +0100
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.3.0

Properties of Random Graphs -- Subgraph Containment
Lars Hupel
Random graphs are graphs with a fixed number of vertices, where each edge is
present with a fixed probability. We are interested in the probability that a
random graph contains a certain pattern, for example a cycle or a clique. A very
high edge probability gives rise to perhaps too many edges (which degrades
performance for many algorithms), whereas a low edge probability might result in
a disconnected graph. We prove a theorem about a threshold probability such that
a higher edge probability will asymptotically almost surely produce a random
graph with the desired subgraph.
http://afp.sourceforge.net/entries/Random_Graph_Subgraph_Threshold.shtml
Enjoy!

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*