Finding models through graph saturation

Sebastiaan J. C. Joosten (Corresponding Author)

Research output: Contribution to journalArticleAcademicpeer-review

7 Downloads (Pure)

Abstract

We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants \tr{}s that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these \tr{}s, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.
Original languageEnglish
Pages (from-to)98-112
Number of pages15
JournalJournal of Logical and Algebraic Methods in Programming
Volume100
DOIs
Publication statusPublished - Nov 2018

Fingerprint

Saturation
Invariant
Graph in graph theory
Chemical analysis
Graph Rewriting
Binary relation
Decision Procedures
Decision problem
Converse
Correctness
Equality
Intersection
Model

Keywords

  • cs.DM
  • cs.PL
  • cs.LO

Cite this

@article{48ae3c3a029542f7a0f75f9aec384f85,
title = "Finding models through graph saturation",
abstract = "We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants \tr{}s that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these \tr{}s, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.",
keywords = "cs.DM, cs.PL, cs.LO",
author = "Joosten, {Sebastiaan J. C.}",
year = "2018",
month = "11",
doi = "10.1016/j.jlamp.2018.06.005",
language = "English",
volume = "100",
pages = "98--112",
journal = "Journal of Logical and Algebraic Methods in Programming",
issn = "2352-2208",
publisher = "Elsevier",

}

Finding models through graph saturation. / Joosten, Sebastiaan J. C. (Corresponding Author).

In: Journal of Logical and Algebraic Methods in Programming, Vol. 100, 11.2018, p. 98-112.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Finding models through graph saturation

AU - Joosten, Sebastiaan J. C.

PY - 2018/11

Y1 - 2018/11

N2 - We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants \tr{}s that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these \tr{}s, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.

AB - We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants \tr{}s that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these \tr{}s, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author.

KW - cs.DM

KW - cs.PL

KW - cs.LO

U2 - 10.1016/j.jlamp.2018.06.005

DO - 10.1016/j.jlamp.2018.06.005

M3 - Article

VL - 100

SP - 98

EP - 112

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -