Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)
Abstract
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.
Cite
Text
Lucas. "Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2020. doi:10.24963/IJCAI.2020/710Markdown
[Lucas. "Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)." International Joint Conference on Artificial Intelligence, 2020.](https://mlanthology.org/ijcai/2020/lucas2020ijcai-proving/) doi:10.24963/IJCAI.2020/710BibTeX
@inproceedings{lucas2020ijcai-proving,
title = {{Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)}},
author = {Lucas, Salvador},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2020},
pages = {5075-5079},
doi = {10.24963/IJCAI.2020/710},
url = {https://mlanthology.org/ijcai/2020/lucas2020ijcai-proving/}
}