We report on the formalization of two classical results about claw-free graphs, which have been verified correct by Jacob T. Schwartz’s proof-checker Referee. We have proved formally that every connected claw-free graph admits (1) a near-perfect matching, (2) Hamiltonian cycles in its square. To take advantage of the set-theoretic foundation of Referee, we exploited set equivalents of the graph-theoretic notions involved in our experiment: edge, source, square, etc. To ease some proofs, we have often resorted to weak counterparts of well-established notions such as cycle, claw-freeness, longest directed path, etc.
Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets / Omodeo, Eugenio; Alexandru I., Tomescu. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - STAMPA. - 52:1(2012), pp. 1-29. [10.1007/s10817-012-9272-3]
Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets
OMODEO, EUGENIO;
2012-01-01
Abstract
We report on the formalization of two classical results about claw-free graphs, which have been verified correct by Jacob T. Schwartz’s proof-checker Referee. We have proved formally that every connected claw-free graph admits (1) a near-perfect matching, (2) Hamiltonian cycles in its square. To take advantage of the set-theoretic foundation of Referee, we exploited set equivalents of the graph-theoretic notions involved in our experiment: edge, source, square, etc. To ease some proofs, we have often resorted to weak counterparts of well-established notions such as cycle, claw-freeness, longest directed path, etc.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
