Skip to Content

Finding models through graph saturation

Posted on

Authors:

  • Joosten, Sebastiaan J. C.

Published in: Journal of Logical and Algebraic Methods in Programming pp 98–112

DOI: 10.1016/j.jlamp.2018.06.005

Paper

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.

BibTeX entry:

@article{Joosten18,
 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.},
 author = {Joosten, {Sebastiaan Jozef Christiaan}},
 doi = {10.1016/j.jlamp.2018.06.005},
 issn = {2352-2208},
 journal = {Journal of Logical and Algebraic Methods in Programming},
 keyword = {cs.LO, cs.DM, cs.PL},
 language = {English},
 month = {11},
 pages = {98--112},
 publisher = {Elsevier BV},
 title = {Finding models through graph saturation},
 volume = {100},
 year = {2018}
}