Provenance Analysis for First-order Model Checking
Is a given finite structure a model of a given first-order sentence? The provenance analysis of this question determines how its 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 (RWTH Aachen University) 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 missing answers for queries, and failures of integrity constraints, as well to compute corresponding repairs that fix these issues. Other collaborators: Abdu Alawini, Jane Xu, and Waley Zhang (UPenn).
2 окт 2024
