Finding models through graph saturation

2018/06/25 by Sebastiaan J. C. Joosten, Joosten, Sebastiaan J. C.
Computer Science · #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.DM #cs.LO #cs.PL

paper · pdf · doi:10.48550/arxiv.1806.09392

arxiv created 2018/06/25 · arxiv updated 2018/06/26

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 \trs 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 \trs, 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.

Related

• Recovering sparse graphs
• A Note on the Modeling Power of Different Graph Types
• Categorical E-Graphs for Lambda Calculi
• Successor-Invariant First-Order Logic on Graphs with Excluded Topological Subgraphs
• Twin-width I: tractable FO model checking