Finding models through graph saturation

June 25, 2018 · The Ethereal · 🏛 J. Log. Algebraic Methods Program.

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Sebastiaan J. C. Joosten arXiv ID 1806.09392 Category cs.LO: Logic in CS Cross-listed cs.DM, cs.PL Citations 2 Venue J. Log. Algebraic Methods Program. Last Checked 5 months ago

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.