Towards Combining Dense Linear Order with Random Graph
Jiamou Liu,
Ting Zhang
Abstract
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, for which there
exists a simple quantifier elimination scheme that uses the elimination
procedures for individual component theories as black boxes. We show
that a good model exists for the union theory of dense linear order and
random graph, and it coincides with the Fraisse limit of the class of finite
graph with ordered vertices.
