Domination Chain with Weighted Parameters (Coq files)
This code contains a formal description of basic facts about Graph Theory and Domination Theory in the language Coq/Ssreflect. It is called DomTheory and consists of: *) The proof that the sum of degrees equals the cardinal of the edge set. *) Definitions and results about open and closed neighborho...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | other conjunto de datos publishedVersion |
| Lenguaje: | Inglés |
| Publicado: |
2020
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/2133/18977 http://hdl.handle.net/2133/18977 |
| Aporte de: |
| Sumario: | This code contains a formal description of basic facts about Graph Theory and Domination Theory in the language Coq/Ssreflect. It is called DomTheory and consists of: *) The proof that the sum of degrees equals the cardinal of the edge set. *) Definitions and results about open and closed neighborhoods, stable sets, dominating sets, irredundant sets, hereditary and superhereditary properties, maximal/minimal sets and sets of maximum/minimum weight. *) The (weighted version of the) Cockayne-Hedetniemi domination chain. *) Examples of proofs with domination parameters on complete graphs. This code also contains: *) A browsable version made with the tool CoqDocJS, with some ''pretty-print'' symbols (like empty set, summation and set comprehension) added later. *) A solver that computes the (unweighted and weighted versions of) parameters gamma, ii, alpha, Gamma and IR. *) (experimental) The solver also generates a Coq file with a proof of alpha(G) >= k, where k is the size of the best stable set found during the optimization. *) A set of instances. |
|---|