Convex sub hypergraphs

[mstn]

Context

Convex sub hypergraphs for rewriting with SMT.

Details

• Modeled a sub hypergraph H of G as an arrow H -> G
• To avoid “all paths” quantification we turned it into reachability in a doubled state space. If layer‑1 reachability intersects the selected node set, convexity fails (credits Codex). In the paper, there is a note saying that convexity can be checked in a more efficient way assuming acyclic and monogamous, we might consider in the future also this case.