Model Completeness, Covers and Superposition

Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, and Andrey Rivkin

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