Peter Baumgartner.
Automatische Inferenz.
In Josef Schneeberger Günther Görz and Ute Schmid, editors, Handbuch der Künstlichen Intelligenz, chapter 5, pages 129-167. Oldenbourg Verlag, 5 edition, 2013. [ bib ]
Peter Baumgartner and Uwe Waldmann.
Hierarchic Superposition: Completeness without Compactness.
In Marek Kosta and Thomas Sturm, editors, MACIS 2013 -Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, pages 8-12, 2013. [ bib | .pdf ]
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.

Peter Baumgartner and Joshua Bax.
Proving Infinite Satisfiability.
In Aart Middeldorp Ken McMillan and Andrei Voronkov, editors, Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19), volume 8312 of Lecture Notes in Artificial Intelligence, pages 68-95. Springer, 2013.
Copyright Springer Verlag [ bib | .pdf ]
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).

Martin Diller Andreas Bauer, Peter Baumgartner and Michael Norrish.
Tableaux for Verification of Data-Centric Processes.
In Didier Galmiche and Dominique Larchey-Wendling, editors, Tableaux 2013 - Automated Reasoning with Analytic Tableaux and Related Methods, volume 8123 of Lecture Notes in Artificial Intelligence, pages 28-43. Springer, 2013.
Copyright Springer Verlag [ bib | .pdf ]
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.

Peter Baumgartner and Uwe Waldmann.
Hierarchic Superposition With Weak Abstraction.
In Maria Paola Bonacina, editor, CADE-24 - The 24th International Conference on Automated Deduction, volume 7898 of Lecture Notes in Artificial Intelligence, pages 39-57. Springer, 2013.
Copyright Springer Verlag [ bib | DOI | .pdf ]
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.