IJCAI 2020poster0 citations
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.
Knowledge Representation and Reasoning: Automated ReasoningTractable Languages and Knowledge compilationKnowledge Representation and Reasoning: Logics for Knowledge RepresentationMultidisciplinary Topics and Applications: Validation and Verification
BibTeX
@inproceedings{ijcai2020p710,
title = {Proving Semantic Properties as First-Order Satisfiability (Extended Abstract)},
author = {Lucas, Salvador},
booktitle = {Proceedings of the Twenty-Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-20}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Christian Bessiere},
pages = {5075--5079},
year = {2020},
month = {7},
note = {Journal track},
doi = {10.24963/ijcai.2020/710},
url = {https://doi.org/10.24963/ijcai.2020/710},
}