@techreport{atr53,
    author      =   {Ernst Althaus and Evgeny Kruglov and Christoph Weidenbach},
    title       =   {Superposition Modulo Linear Arithmetic SUP(LA)},
    editor      =   {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
                    Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
                    Wilhelm},
    institution =   {SFB/TR 14 AVACS},
    subproject  =   {H1/2},
    year        =   {2009},
    month       =   {December},
    type        =   {Reports of SFB/TR 14 AVACS},
    series      =   {ATR},
    number      =   53,
    note        =   {ISSN: 1860-9821, http://www.avacs.org.},
    access      =   {open},
    abstract    =   {The hierarchical superposition based theorem proving 
                     calculus of Bachmair, Ganzinger, and Waldmann enables 
                     the hierarchic combination of a theory with full 
                     first-order logic. If a clause set of the combination 
                     enjoys a sufficient completeness criterion, the calculus 
                     is even complete. We instantiate and refine the calculus 
                     for the theory of linear arithmetic. In particular, we 
                     develop new effective versions for the standard 
                     superposition redundancy criteria taking the linear 
                     arithmetic theory into account.  The resulting calculus 
                     is implemented in SPASS(LA) and extends 
                     the state of the art in proving properties of first-order 
                     formulas over linear arithmetic.},
    bibtex      =   {atr053.bib},
    pdf         =   {avacs_technical_report_053.pdf}
}