Towards combining dense linear order with random graphs
| aut.researcher | Liu, Jiamou | |
| dc.contributor.author | Liu, J | |
| dc.contributor.author | Zhang, T | |
| dc.date.accessioned | 2011-11-27T03:52:57Z | |
| dc.date.available | 2011-11-27T03:52:57Z | |
| dc.date.copyright | 2008-08-10 | |
| dc.date.issued | 2008-08-10 | |
| dc.description.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, 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. | |
| dc.identifier.citation | 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 | |
| dc.identifier.uri | https://hdl.handle.net/10292/2813 | |
| dc.publisher | 4th International Joint Conference on Automated Reasoning (IJCAR 2008) | |
| dc.relation.uri | http://www.mpi-inf.mpg.de/~sofronie/cedar08-program.html | |
| dc.relation.uri | http://www.mpi-inf.mpg.de/~sofronie/proceedings-cedar08.pdf | |
| dc.rights | 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. | |
| dc.rights.accessrights | OpenAccess | |
| dc.title | Towards combining dense linear order with random graphs | |
| dc.type | Conference Contribution | |
| pubs.organisational-data | /AUT | |
| pubs.organisational-data | /AUT/Design & Creative Technologies | |
| pubs.organisational-data | /AUT/Design & Creative Technologies/School of Computing & Mathematical Science | |
| pubs.organisational-data | /AUT/PBRF Researchers | |
| pubs.organisational-data | /AUT/PBRF Researchers/Design & Creative Technologies PBRF Researchers | |
| pubs.organisational-data | /AUT/PBRF Researchers/Design & Creative Technologies PBRF Researchers/DCT C & M Computing |