2026-08-10T21:52:43Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11091 2024-03-06T10:47:20Z ddc:004 open_access

Formalization of the Domination Chain with Weighted Parameters (Short Paper) Severín, Daniel E. Domination Chain Coq Formalization of Mathematics The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters of graph theory: for a given graph G, ir(G) <= gamma(G) <= iota(G) <= alpha(G) <= Gamma(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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Daniel E. Severín 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.36 urn:nbn:de:0030-drops-110919 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.36 eng https://creativecommons.org/licenses/by/3.0/legalcode