Mechanising Hall’s Theorem for Countable Graphs

EasyChair Preprint no. 10365

Abstract

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

@Booklet{EasyChair:10365,
  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}}