Abstract

Model-checking for first-order logic is the computational problem of deciding whether a given finite structure is a model of a given first-order sentence. Its provenance analysis determines how that answer depends on the atomic facts that determine the structure. Provenance questions like this one have emerged in databases, scientific workflows, networks, formal verification, and other areas.

In joint work with Erich Grädel, done during the Logical Structures in Computation Program at the Simons Institute, we extend the semiring provenance framework, developed in databases, to the first-order model checking problem. This provides a non-standard semantics for first-order logic that refines logical truth to values in commutative semirings: a semiring of provenance polynomials, the Viterbi semiring of confidence scores, access control semirings, etc. The semantics can be used to synthesize models based on criteria like maximum confidence or public access. Our uniform treatment of logical negation can be used to explain absent answers for queries, and failures of integrity constraints, as well to compute corresponding “repairs” to a model to fix these issues.

The work on repairs is also joint with Abdu Alawini, Jane Xu, and Waley Zhang.