# peter-2007.bib

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

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

@inproceedings{Baumgartner:Furbach:Pelzer:HyperTableauxEquality:CADE:2007,
author = {Peter Baumgartner and Ulrich Furbach and Bj\"orn Pelzer},
title = {Hyper Tableaux with Equality},
url = {ehyper.pdf},
pages = {492-507},
era = {A},
booktitle = {CADE-21 -- The 21st International Conference on Automated
Deduction},
editor = {Frank Pfenning},
year = {2007},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
volume = {4603},
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 treatment 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
paramodulation are drawn (only) from a set of positive unit clauses,
the candidate model. The
calculus also features a generic, semantically justified
simplification rule which covers many redundancy elimination techniques
known from superposition-style theorem proving.
Our main theoretical result is the soundness and completeness of the
calculus. The calculus is implemented, and we also report on
practical experiments.}
}

@inproceedings{Baumgartner:LogicalEngineeringInstanceBasedMethods:CADE:2007,
author = {Peter Baumgartner},
title = {Logical Engineering with Instance-Based Methods},
url = {LEIM.pdf},
era = {A},
booktitle = {CADE-21 -- The 21st International Conference on Automated
Deduction},
editor = {Frank Pfenning},
month = {July},
year = {2007},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
volume = {4603},
pages = {404-409}
}

@proceedings{CADE:07,
booktitle = {CADE-21 -- The 21st International Conference on Automated
Deduction},
editor = {Frank Pfenning},
year = {2007},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
volume = {4603},
title = {Automated Deduction -- CADE-21}
}