peter-2013.bib
@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -c 'year=2013 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2013.bib -oc peter-2013.cite peter.bib}}
@incollection{Baumgartner:AutomatischeInferenz:KIHandbuch:2013,
author = {Peter Baumgartner},
title = {Automatische Inferenz},
chapter = {5},
publisher = {Oldenbourg Verlag},
year = {2013},
booktitle = {Handbuch der K\"unstlichen Intelligenz},
editor = {G\"unther G\"orz, Josef Schneeberger and Ute Schmid},
pages = {129--167},
edition = {5}
}
@inproceedings{Baumgartner:Waldmann:HSPCompletenessWithoutCompactness:MACIS:2013,
author = {Peter Baumgartner and Uwe Waldmann},
title = {Hierarchic Superposition: Completeness without Compactness},
booktitle = {MACIS 2013 --Fifth International Conference on Mathematical Aspects of Computer and Information Sciences},
editor = {Marek Kosta and Thomas Sturm},
year = {2013},
abstract = {Many applications of automated deduction and verification require reasoning in
combinations of theories, such as, on the one hand (some fragment of)
first-order logic, and on, the other hand a background theory, such as some
form of arithmetic. Unfortunately, due to the high expressivity of the full
logic, complete reasoning is impossible in general. It is a
realistic goal, however, to devise theorem provers that are ``reasonably
complete'' in practice, and the hierarchic superposition calculus has been designed as a
theoretical basis for that. In a recent paper we
introduced an extension of hierarchic superposition and proved its
completeness for the fragment where every term of the background sort is
ground. In this paper, we extend this result and obtain completeness for a
larger fragment that admits variables in certain places.},
pages = {8--12},
url = {hsp-macis-2013.pdf}
}
@inproceedings{Baumgartner:Bax:ProvingInfiniteSatisfiability:LPAR:2013,
author = {Peter Baumgartner and Joshua Bax},
title = {Proving Infinite Satisfiability},
booktitle = {Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19)},
editor = {Ken McMillan, Aart Middeldorp and Andrei Voronkov},
year = {2013},
volume = {8312},
series = {Lecture Notes in Artificial Intelligence},
pages = {68--95},
publisher = {Springer},
url = {LPAR-19-final.pdf},
abstract = {We consider the problem of automatically disproving invalid conjectures over data
structures such as lists and arrays over integers, in the presence of additional
hypotheses over these data structures.
We investigate a simple approach based on refutational theorem
proving. We assume that the data structure axioms are satisfiable and provide a
template language for additional hypotheses such that satisfiability is
preserved. Then, disproving is done by proving that the negated conjecture
follows. By means of examples, we demonstrate that our template language is
reasonably expressive and that our approach works well with current theorem provers
(Z3, SPASS+T and Beagle).},
copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}}
}
@inproceedings{Bauer:etal:TableauxDataCentricProcesses:TABLEAUX:2013,
author = {Andreas Bauer, Peter Baumgartner, Martin Diller and Michael Norrish},
title = {Tableaux for Verification of Data-Centric Processes},
booktitle = {Tableaux 2013 -- Automated Reasoning with Analytic Tableaux and Related Methods},
editor = {Didier Galmiche and Dominique Larchey-Wendling},
year = {2013},
volume = {8123},
series = {Lecture Notes in Artificial Intelligence},
pages = {28--43},
publisher = {Springer},
url = {PCBRP-TABLEAUX-2013.pdf},
copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
abstract = {Current approaches to analyzing dynamic systems are mostly
grounded in propositional (temporal) logics. As a
consequence, they often lack expressivity for modelling rich
data structures and reasoning about them in the course of a
computation. To address this problem, we propose a rich
modelling framework based on first-order logic over
background theories (arithmetics, lists, records, etc) and
state transition systems over corresponding interpretations.
On the reasoning side, we introduce a tableau calculus for
bounded model checking of properties expressed in a certain
fragment of CTL* over that first-order logic. We also
describe a k-induction scheme on top of that calculus for
proving safety properties, and we report on first
experiments with a prototypical implementation.}
}
@inproceedings{Baumgartner:Waldmann:HSPWeakAbstraction:CADE:2013,
author = {Peter Baumgartner and Uwe Waldmann},
title = {Hierarchic Superposition With Weak Abstraction},
booktitle = {CADE-24 -- The 24th International Conference on Automated
Deduction},
editor = {Maria Paola Bonacina},
year = {2013},
doi = {10.1007/978-3-642-38574-2_3},
series = {Lecture Notes in Artificial Intelligence},
copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
pages = {39-57},
volume = {7898},
publisher = {Springer},
copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
url = {MPI-I-2013-RG1-002.pdf},
abstract = {Many applications of automated deduction require reasoning in first-order logic
modulo background theories, in particular some form of integer arithmetic. A major
unsolved research challenge is to design theorem provers that are ``reasonably
complete'' even in the presence of free function symbols ranging into a background
theory sort. The hierarchic superposition calculus
of Bachmair, Ganzinger, and Waldmann already supports such
symbols, but, as we demonstrate, not optimally. This paper aims to rectify the
situation by introducing a novel form of clause abstraction, a core component in the
hierarchic superposition calculus for transforming clauses into a form
needed for internal operation. We argue for the benefits of the resulting calculus
and provide a new
completeness result for the fragment where all background-sorted terms are ground.}
}