peter-2010.bib

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

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

@proceedings{Armando:Baumgartner:Dowek:IJCAR2008JarSpecialIssue:JAR:2010,
  title = {Special Issue: Selected Papers from the 4th International 
Joint Conference on Automated Reasoning},
  year = {2010},
  optkey = {},
  optbooktitle = {},
  editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
  volume = {45},
  number = {2},
  era = {A},
  series = {Journal of Automated Reasoning},
  copyright = {Copyright Springer Verlag \url{http://www.springer.com/}},
  optaddress = {},
  url = {http://springerlink.com/content/mt7505055125/},
  month = {August},
  optorganization = {},
  publisher = {Springer},
  note = {ISSN 0168-7433 (Print) 1573-0670 (Online)},
  optannote = {}
}

@article{Baumgartner:Furbach:Pelzer:HyperTableauxCalculusEquality:2010,
  author = {Peter Baumgartner and Ulrich Furbach and Bj\"orn Pelzer},
  title = {The Hyper Tableaux Calculus with Equality and an 
Application to Finite Model Computation},
  journal = {Journal of Logic and Computation},
  url = {ehyper-long.pdf},
  year = {2010},
  era = {A},
  abstract = {In most theorem proving applications, a proper
                  treatment of equational theories or equality is
                  mandatory. In this paper we show how to integrate a
                  modern treat- ment of equality in the hyper tableau
                  calculus. It is based on splitting of positive
                  clauses and an adapted version of the superposition
                  inference rule, where equations used for
                  superposition are drawn (only) from a set of
                  positive unit clauses, and superposition
                  inferences into positive literals is restricted into
                  (positive) unit clauses only. The calculus also
                  features a generic, semantically justified
                  simplification rule which covers many redundancy
                  elimination techniques known from superposition
                  theorem proving. Our main results are soundness and
                  completeness of the calculus, but we also show how
                  to apply the calculus for finite model computation,
                  and we briefly describe the implementation.},
  volume = {20},
  number = {1},
  pages = {77-109},
  month = {February},
  doi = {10.1093/logcom/exn061},
  optannote = {}
}

@article{Baumgartner:Thorstensen:IMOverview:2010,
  author = {Peter Baumgartner and Evgenij Thorstensen},
  title = {Instance Based Methods --- A Brief Overview},
  journal = {KI - K\"unstliche Intelligenz},
  optkey = {},
  volume = {24},
  issue = {1},
  pages = {35-42},
  month = {April},
  year = {2010},
  abstract = {Instance-based methods are a specific class of methods
                  for automated proof search in first-order
                  logic. This article provides an overview of the
                  major methods in the area and discusses their
                  properties and relations to the more established
                  resolution methods. It also discusses some recent
                  trends on refinements and applications. This
                  overview is rather brief and informal, but we
                  provide a comprehensive literature list to follow-up
                  on the details.},
  url = {IMoverview.pdf},
  issn = {0933-1875},
  doi = {10.1007/s13218-010-0002-x}
}