Proving semantic properties as first-order satisfiability

[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.Partially supported by the EU (FEDER), and projects RTI2018-094403-B-C32, PROMETE0/2019/098, and SP20180225.Lucas Alba, S. (2019). Proving semantic properties as first-order satisfiability. Artificial Intelligence. 277:1-24. https://doi.org/10.1016/j.artint.2019.10317412427