Model Completeness, Covers and Superposition

Proc. of the 27th Int. Conf. on Automated Deduction (CADE). 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)",
   pages = "142--160",
   volume = "11716",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-030-29436-6_9",
}