Proving Semantic Properties as First-Order Satisfiability

The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, goals, and claims about the behavior or features of the system can be expressed as formulas phi which should be checked with respect to the intended model of Th, which is often huge or even incomputable. In this paper we show how to prove such semantic properties phi of Th by just finding a model A of Th boolean OR {phi} boolean OR Z(phi), where Z(phi) is an appropriate (possibly empty) theory depending on phi only. Applications to relational and deductive databases, rewriting-based systems, logic programming, and answer set programming are discussed.