@comment{{This file has been generated by bib2bib 1.95}}

@comment{{Command line: bib2bib -c 'year=2011 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2011.bib -oc peter-2011.cite peter.bib}}

@inproceedings{Baumgartner:Tinelli:MEET:CADE:2011, author = {Peter Baumgartner and Cesare Tinelli}, title = {Model Evolution with Equality Modulo Built-in Theories}, booktitle = {CADE-23 -- The 23nd International Conference on Automated Deduction}, editor = {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans}, year = {2011}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, volume = {6803}, pages = {85--100}, copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}}, era = {A}, url = {MEET-draft.pdf}, abstract = {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 arithmetic. The new calculus is an extension of the Model Evolution Calculus with Equality, a first-order logic version of the propositional DPLL procedure, including its ordering-based redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete under certain conditions.} }

@article{Baumgartner:Waldmann:MESUP:JAR:2011, author = {Peter Baumgartner and Uwe Waldmann}, title = {A Combined Superposition and Model Evolution Calculus}, journal = {Journal of Automated Reasoning}, copyright = {Copyright Springer Verlag http://www.springer.com/}, year = {2011}, optkey = {}, url = {MESUP-long.pdf}, doi = {10.1007/s10817-010-9214-x}, volume = {47}, number = {2}, pages = {191-227}, month = {August}, abstract = {We present a new calculus for first-order theorem proving with equality, ME+SUP, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivial way. The main motivation is to combine the advantageous features of these two rather complementary calculi in a single framework. In particular, Model Evolution, as a lifted version of the propositional DPLL procedure, contributes a non-ground splitting rule that effectively permits to split a clause into non variable disjoint subclauses. In the paper we present the calculus in detail. Our main result is its completeness under semantically justified redundancy criteria and simplification rules. We also show how under certain assumptions the model representation computed by a (finite and fair) derivation can be queried in an effective way.}, era = {A} }

@proceedings{CADE:11, booktitle = {CADE-23 -- The 23nd International Conference on Automated Deduction}, editor = {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans}, year = {2011}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, volume = {6803} }