|
Abstract : |
Abstract. This paper extends a calculus for first-order logic that combines the inference mechanism of hyperresolution with the more informative structure of analytic tableaux and that has been introduced as hyper tableaux by Baumgartner et al. (1996). This clausal tableau calculus is proof confluent, but suffers from the need of partial ground instantiations. I will develop an improvement of hyper tableaux which avoids this by using full unification with rigid variables, but keeps desirable features like proof confluence and a partially universal treatment of variables in a clausal tableau. The resulting calculus can be seen as a refined hyperresolution calculus that deals properly with an arbitrary literal selection function without loss of completeness. For this calculus, I have implemented and evaluated a proof procedure which takes advantage of proof confluence and addresses the fairness problem of tableau caluli with a redundancy criterion based upon literal subsumption. 1, |
