Baumgartner, PeterWaldmann, Uwe2015-12-10June 9-149783642385735http://hdl.handle.net/1885/66295Many 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" evenKeywords: Automated deduction; Background theory; First order logic; Function symbols; Integer arithmetic; Internal operations; Research challenges; Superposition calculus; Abstracting; Automation; Calculations; Theorem proving; Automata theoryHierarchic Superposition with Weak Abstraction201310.1007/978-3-642-38574-2_32016-02-24