peter-2011.bib

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

@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}
}