CONSOLUTION AS A FRAMEWORK FOR COMPARING CALCULI

Authors
BAUMGARTNER P FURBACH U
Citation
P. Baumgartner et U. Furbach, CONSOLUTION AS A FRAMEWORK FOR COMPARING CALCULI, Journal of symbolic computation, 16(5), 1993, pp. 445-477
Citations number
23
Categorie Soggetti
Mathematics,"Computer Sciences, Special Topics",Mathematics,"Computer Science Theory & Methods
Journal title
Journal of symbolic computation → ACNP
ISSN journal
07477171
Volume
16
Issue
5
Year of publication
1993
Pages
445 - 477
Database
ISI
SICI code
0747-7171(1993)16:5<445:CAAFFC>2.0.ZU;2-5
Abstract
In this paper, stepwise and nearly stepwise simulation results for a n umber of first-order proof calculi are presented and an overview is gi ven that illustrates the relations between these calculi. For this pur pose, we modify the consolution calculus in such a way that it can be instantiated to resolution, tableaux model elimination, a connection m ethod and Loveland's model elimination.