Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe
Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. In this paper we consider the case when all variables occurring below such function symbols are quantified over a finite subset of their domains. We present a...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.