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 sentences 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 sentences, 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 sentences 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 sentences, 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}},
 bdsk-url-1 = {https://doi.org/10.1016/j.jlamp.2018.06.005},
 date-modified = {2018-11-23 10:32:45 +0100},
 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}
}