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]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.