Email Gateway (Aug 22 2022 at 18:48): Email Gateway (Aug 22 2022 at 18:48):From: Tobias Nipkow <nipkow@in.tum.de>
Graph Saturation
Sebastiaan J. C. Joosten
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.
https://www.isa-afp.org/entries/Graph_Saturation.html
Enjoy!
smime.p7s
Last updated: Apr 20 2024 at 08:16 UTC