Combined Covers and Beth Definability

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

Proc. of the 10th Int. Joint Conf. on Automated Reasoning (IJCAR 2020). Volume 12166 of Lecture Notes in Computer Science. 2020.

Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as "covers") in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that cover may not exist in the combined theories, even in case combined quantifier-free interpolant do exist.


@inproceedings{IJCAR-2020,
   title = "Combined Covers and Beth Definability",
   year = "2020",
   author = "Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and
Marco Montali and Andrey Rivkin",
   booktitle = "Proc. of the 10th Int. Joint Conf. on Automated Reasoning
(IJCAR 2020)",
   pages = "181--200",
   volume = "12166",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-030-51074-9_11",
}
pdf