Proving semantic properties as first-order satisfiability

Abstract

[EN] 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 ¿ 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 ¿ of Th by just finding a model A of Th¿{¿}¿Z¿, where Z¿ is an appropriate (possibly empty) theory depending on ¿ only. Applications to relational and deductive databases, rewriting-based systems, logic programming, and answer set programming are discussed.