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 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.本代码以Coq/Ssreflect语言形式化描述了图论与支配理论的基础内容，该形式化库名为DomTheory，其包含以下内容： *) 顶点度数之和等于边集基数的证明； *) 关于开邻域、闭邻域、独立集、支配集、无冗余集、遗传与超遗传性质、极大/极小集以及最大/最小权集的定义与相关结论； *) Cockayne-Hedetniemi支配链（含权版本）； *) 完整图上支配参数的证明示例。 本代码还包含以下内容： *) 使用CoqDocJS工具生成的可浏览版本，后续补充了部分美化打印符号（如空集、求和符号与集合推导式）； *) 可计算参数γ、ii、α、Γ与IR的无权与带权版本求解器； *) （实验性功能）该求解器还可生成包含α(G)≥k证明的Coq文件，其中k为优化过程中找到的最优独立集的规模； *) 一组测试用例。