2020-09-212020-09-212019978-3-95977-122-11868-8969http://hdl.handle.net/2133/18978The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters of graph theory: for a given graph G, ir(G) ≤ γ(G) ≤ ι(G) ≤ α(G) ≤ Γ(G) ≤ IR(G). These parameters return the maximum/minimum cardinality of a set satisfying some property. However, they can be generalized for graphs with weighted vertices where the objective is to maximize/minimize the sum of weights of a set satisfying the same property, and the domination chain still holds for them. In this work, the definition of these parameters as well as the chain is formalized in Coq/Ssreflect.application/pdfengopenAccessMathematics of computingGraph theoryhttps://purl.org/becyt/ford/1.1Domination ChainCoqFormalization of MathematicsconferenceObjectAutorhttps://creativecommons.org/licenses/by/3.0/