Towards combining dense linear order with random graphs

Le résumé fourni par la source

In this paper we present our work in progress towards obtaining a Nelson-Oppen style combination for combining quantified theories, where each individual component theory admits quantifier elimination. We introduces the notion of good model for union theories, and show that for the good models of union theories, there exists a simple quantifier elimination scheme which uses the elimination procedures for individual component theories as black boxes. Using a priority argument, we show that good models exist for the union theory of dense linear order and random graph.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.