Finding models through graph saturation

Sebastiaan J. C. Joosten (Corresponding Author)

    Research output: Contribution to journalArticleAcademicpeer-review

    1 Citation (Scopus)
    100 Downloads (Pure)


    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
    Publication statusPublished - Nov 2018


    • cs.DM
    • cs.PL
    • cs.LO
    • n/a OA procedure


    Dive into the research topics of 'Finding models through graph saturation'. Together they form a unique fingerprint.

    Cite this