Download PDFOpen PDF in browser

Mechanising Hall’s Theorem for Countable Graphs

EasyChair Preprint no. 10365

14 pagesDate: June 9, 2023


This work presents a formalisation in Isabelle/HOL of the extension of Hall's theorem for finite graphs to countable graphs. The proof uses a formalisation of the authors' countable set-theoretical version of Hall's theorem that was proved as a consequence of the marriage-condition characterisation for finite families of sets and a formalisation in Isabelle/HOL of the compactness theorem for propositional logic.
 The development focuses on maintaining specifications and proofs as closely as possible to textbooks since our primary objective is to increase mathematicians' interest in using interactive proof assistants. Although this, the specification also includes a concise and more automatised proof using locales.
 The development is a first step toward mechanising infinite versions of results equivalent to Hall's marriage theorem in contexts other than set theory.

Keyphrases: Countable Graphs, Hall's Theorem, interactive theorem proving, Isabelle/HOL

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Fabián Fernando Serrano Suárez and Mauricio Ayala-Rincón and Thaynara Arielly de Lima},
  title = {Mechanising Hall’s Theorem for Countable Graphs},
  howpublished = {EasyChair Preprint no. 10365},

  year = {EasyChair, 2023}}
Download PDFOpen PDF in browser