Skip navigation
Skip navigation

Model Evolution with Equality Modulo Built-in Theories

Baumgartner, Peter; Tinelli, Cesare


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]

CollectionsANU Research Publications
Date published: 2011
Type: Conference paper
Source: Proceedings of International Conference on Automated Deduction (CADE 2009)
DOI: 10.1007/978-3-642-22438-6_9


File Description SizeFormat Image
01_Baumgartner_Model_Evolution_with_Equality_2011.pdf285.96 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator