Graph Saturation

Research output: Contribution to journalArticleAcademicpeer-review

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.
Original languageEnglish
Number of pages89
JournalArchive of Formal Proofs
Volume2018
Publication statusPublished - 23 Nov 2018

Cite this

@article{80db3427682c47e1982a552413a2f868,
title = "Graph Saturation",
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.",
author = "Joosten, {Sebastiaan Jozef Christiaan}",
year = "2018",
month = "11",
day = "23",
language = "English",
volume = "2018",
journal = "Archive of Formal Proofs",
issn = "2150-914x",
publisher = "SourceForge",

}

Graph Saturation. / Joosten, Sebastiaan Jozef Christiaan.

In: Archive of Formal Proofs, Vol. 2018, 23.11.2018.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Graph Saturation

AU - Joosten, Sebastiaan Jozef Christiaan

PY - 2018/11/23

Y1 - 2018/11/23

N2 - 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.

AB - 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.

M3 - Article

VL - 2018

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

SN - 2150-914x

ER -