Skip to main content

Questions tagged [graphs]

A graph is a collection of vertices and edges; each edge links a pair of vertices, defining a relationship of incidence between vertices and edges. (from nLab)

Filter by
Sorted by
Tagged with
1 vote
0 answers
44 views

how to inductively define paths from paths using unimath

I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(...
noCrayCray's user avatar
2 votes
0 answers
214 views

Lean proofs for graph algorithms

I am new to lean but am interested in proving correctness of graph algorithms. Is there a repository/website that talks about a proof using lean of Dijkstra's shortest path algorithm, for example?
Simd's user avatar
  • 121
1 vote
1 answer
79 views

Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?

The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows. For example, if an arrow is two-headed I need in Coq locally to ...
HighAsAKiteOnMath's user avatar
8 votes
0 answers
168 views

Graph algorithms in Coq

We’re looking for a good library for reasoning about graphs in Coq. Some key features with would want to support include: Topological sorting (ideally along with other graph algorithms) Manipulation ...
Adrian's user avatar
  • 81
4 votes
2 answers
191 views

Can a proof engine be built based on graphs?

One of the more common ways to do proofs is using a deductive system. Can proofs instead be done using graphs? I am seeking papers that outline from the ground up how such a system works. If example ...
Guy Coder's user avatar
  • 2,846