Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Socher-Ambrosius, Rolfdblp

BibTeX cite key*:

socher91c

Title

Title*:

On the Relation Between Completion Based and Resolution Based Theorem Proving

Journal

Journal Title*:

Journal of Symbolic Computation
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:


Publisher's URL:


Publisher's
Address:


ISSN:


Vol, No, pp, Date

Volume*:

11
Number:

1 & 2

Publishing Date:

1991

Pages*:

129-148
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

Completion Theorem Proving, as proposed by Hsiang, is based on the observation that proving a first-order formula is equivalent to solving an equational system over a boolean polynomial ring. The latter can be accomplished by completing the set of rewrite rules obtained from the equational system. This method's basic deduction rule is the generation of a new rule from a divergent critical pair obtained by superposition of two rules. This paper relates superpositiexactly once-a result which was given by R. Shostak-but admit completion refutations with this property, that is, such a completion refutation is shorter than any resolution refutation can be. Furthermore, we show by means of Shostak's theorem that the language of rings and ideals is well suited for short and elegant proofs of theorems about resolution deductions.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:


BibTeX Entry:
@ARTICLE{socher91c,
AUTHOR = {Socher-Ambrosius, Rolf},
 TITLE = {On the Relation Between Completion Based and Resolution Based Theorem Proving},
 JOURNAL = {Journal of Symbolic Computation},
 YEAR = {1991},
 NUMBER = {1 & 2},
 VOLUME = {11},
 PAGES = {129--148},
}

Entry last modified by Uwe Brahm, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm		Created
01/14/1995 06:52:37 PM
Revisions
4.
3.
2.
1.
0.		Editor(s)
Uwe Brahm
Christine Kiesel/AG2/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE		Edit Dates
24.04.97 16:54:58
03/02/95 16:55:08
21/01/95 20:55:38
17/01/95 20:10:26
14/01/95 19:00:53