Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors.
Special Issue: Selected Papers from the 4th International Joint Conference on Automated Reasoning, volume 45 of Journal of Automated Reasoning. Springer, August 2010.
ISSN 0168-7433 (Print) 1573-0670 (Online). [ bib | http ]
 
Peter Baumgartner and Evgenij Thorstensen.
Instance Based Methods - A Brief Overview.
KI - Künstliche Intelligenz, 24:35-42, April 2010. [ bib | DOI | .pdf ]
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.

 
Peter Baumgartner, Ulrich Furbach, and Björn Pelzer.
The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation.
Journal of Logic and Computation, 20(1):77-109, February 2010. [ bib | DOI | .pdf ]
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.