### Abstract

This is an Isabelle/HOL formalisation of graph saturation, closely following a paper by the author on graph saturation. Nine out of ten lemmas of the original paper are proven in this formalisation. The formalisation additionally includes two theorems that show the main premise of the paper: that consistency and entailment are decided through graph saturation. This formalisation does not give executable code, and it did not implement any of the optimisations suggested in the paper.

### License

BSD License

### Topics

- Logic/Rewriting
- Mathematics/Graph theory

### Session Graph_Saturation

- MissingRelation
- LabeledGraphs
- RulesAndChains
- GraphRewriting
- LabeledGraphSemantics
- StandardModels
- RuleSemanticsConnection
- StandardRules
- CombinedCorrectness

## Cite

×

Graph_Saturation-AFP

    @article{Graph_Saturation-AFP,
      author  = {Sebastiaan J. C. Joosten},
      title   = {Graph Saturation},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Graph_Saturation.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Nov 28, 2018 : Isabelle2018