“Relational Constraint Solving in SMT” by Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. In Proceedings of the 26^th International Conference on Automated Deduction (CADE '17), (Leonardo de Moura, ed.), Aug. 2017, pp. 148-165. Gothenburg, Sweden.
Relational logic is useful for reasoning about computational problems with relational structures, including high-level system design, architectural con- figurations of network systems, ontologies, and verification of programs with linked data structures. We present a modular extension of an earlier calculus for the theory of finite sets to a theory of finite relations with such operations as transpose, product, join, and transitive closure. We implement this extension as a theory solver of the SMT solver CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling use cases. For instance, native support for relations enables a natural mapping from Alloy, a declarative modeling language based on first-order relational logic, to SMT constraints. It also enables a natural encoding of several description logics with concrete domains, allowing the use of an SMT solver to analyze, for instance, Web Ontology Language (OWL) models. We provide an initial evaluation of our solver on a number of Alloy and OWL models which shows promising results.
BibTeX entry:
@inproceedings{MRT+17,
author = {Baoluo Meng and Andrew Reynolds and Cesare Tinelli and Clark
Barrett},
editor = {Leonardo de Moura},
title = {Relational Constraint Solving in SMT},
booktitle = {Proceedings of the {\it 26^{th}} International Conference
on Automated Deduction (CADE '17)},
series = {Lecture Notes in Artificial Intelligence},
volume = {10395},
pages = {148--165},
publisher = {Springer},
month = aug,
year = {2017},
note = {Gothenburg, Sweden},
url = {http://theory.stanford.edu/~barrett/pubs/MRT+17.pdf}
}
(This webpage was created with bibtex2web.)