Proc. of the 27th Int. Conf. on Automated Deduction (CADE 2019). Volume 11716 of Lecture Notes in Computer Science. 2019.
In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle infinite-state model checking problems. Motivated by applications to the verification of data-aware processes, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus, equipped with appropriate settings and reduction strategies.
@inproceedings{CADE-2019, title = "Model Completeness, Covers and Superposition", year = "2019", author = "Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin", booktitle = "Proc. of the 27th Int. Conf. on Automated Deduction (CADE 2019)", pages = "142--160", volume = "11716", publisher = "Springer", series = "Lecture Notes in Computer Science", doi = "10.1007/978-3-030-29436-6_9", }pdf