The Inverse Method is a Good Fit for Datalog Theorem Proving

The inverse method on first glance feels like an oddball. But actually it is rather straightforward when viewed from a datalog lens. The inverse method is a bottom up theorem proving method (typically for a sequent calculus) that finds demand for judgements by inspecting the input formula and using the subformula property of the cut-free sequent calculus. It is very schematically similar / identical to datalog methods for demand or magic set. The main thing that is a little annoying is you probably want a first class set for storing contexts $\Gamma$

www.philipzucker.com · Hey There Buddo!