Model Evolution with Equality Modulo Built-in Theories
Many applications of automated deduction require reasoning modulo background theories, in particular some form of integer arithmetic. Developing corresponding automated reasoning systems that are also able to deal with quantified formulas has recently been an active area of research. We contribute to this line of research and propose a novel instantiation-based method for a large fragment of first-order logic with equality modulo a given complete background theory, such as linear integer...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of International Conference on Automated Deduction (CADE 2009)|
|01_Baumgartner_Model_Evolution_with_Equality_2011.pdf||285.96 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.