License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.36
URN: urn:nbn:de:0030-drops-110919
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11091/
Go to the corresponding LIPIcs Volume Portal

Severín, Daniel E.

Formalization of the Domination Chain with Weighted Parameters (Short Paper)

pdf-format:
LIPIcs-ITP-2019-36.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{severn:LIPIcs:2019:11091,
  author =	{Daniel E. Sever{\'\i}n},
  title =	{{Formalization of the Domination Chain with Weighted Parameters (Short Paper)}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{36:1--36:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11091},
  URN =		{urn:nbn:de:0030-drops-110919},
  doi =		{10.4230/LIPIcs.ITP.2019.36},
  annote =	{Keywords: Domination Chain, Coq, Formalization of Mathematics}
}

Keywords: Domination Chain, Coq, Formalization of Mathematics
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The Coq formalization and the solver accompanying this paper can be found at https://dx.doi.org/10.17632/h5j5rvrz2r.2.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI