Towards combining dense linear order with random graphs

Liu, J
Zhang, T
Item type
Conference Contribution
Degree name
Journal Title
Journal ISSN
Volume Title
4th International Joint Conference on Automated Reasoning (IJCAR 2008)

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.

Presentation at Complexity, Expressibility, and Decidability in Automated Reasoning (CEDAR'08), an affiliated workshop of IJCAR 2008, Sydney, Australia, Session 4: Reasoning in complex theories
Rights statement
Auckland University of Technology (AUT) encourages public access to AUT information and supports the legal use of copyright material in accordance with the Copyright Act 1994 (the Act) and the Privacy Act 1993. Unless otherwise stated, copyright material contained on this site may be in the intellectual property of AUT, a member of staff or third parties. Any commercial exploitation of this material is expressly prohibited without the written permission of the owner.