@tmyklebu @pervognsen As you probably know, transitive closure is inexpressible in first-order logic (a fun exercise with the compactness theorem), and adding it to FOL quickly leads to undecidability. Finding decidable fragments of reachability was once a hot research area, but seems to have died off. Here's one of the last big publications from that line of work: https://csaws.cs.technion.ac.il/~shachari/dl/popl2014.pdf
=> More informations about this toot | View the thread | More toots from zwarich@hachyderm.io
=> View tmyklebu@mastodon.gamedev.place profile | View pervognsen@mastodon.social profile
text/geminiThis content has been proxied by September (ba2dc).