Towards combining dense linear order with random graphs
Liu, J; Zhang, T
MetadataShow full metadata
In this paper we present our work in progress towards obtaining a Nelson-Oppen style combination for combining quantiﬁed theories, where each individual component theory admits quantiﬁer 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 quantiﬁer 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.
DateAugust 10, 2008
SourcePresentation at Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08), an affiliated workshop of IJCAR 2008, Sydney, Australia, Session 4: Reasoning in complex theories
Item TypeConference Contribution
Publisher4th International Joint Conference on Automated Reasoning (IJCAR 2008)