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

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