Publications: Journal Article: On Using Ground Joinable Equations in Equational Theorem Proving

Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

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

Action:

Options:

Goto entry point

Author, Editor(s)

Author(s):

Avenhaus, Jürgen
Hillenbrand, Thomas
Löchner, Bernd

dblp
dblp
dblp

Not MPG Author(s):

Avenhaus, Jürgen
Löchner, Bernd

BibTeX cite key*:

AvenhausHillenbrandLoechner2003

Title

Title*:	On Using Ground Joinable Equations in Equational Theorem Proving
Attachment(s):	gjoin.ps (263.96 KB)

Journal

Journal Title*:	Journal of Symbolic Computation	Journal's URL:	http://www.elsevier.com/locate/issn/0747-7171
Download URL for the article:		Language:	English

Publisher

Publisher's Name:	Elsevier	Publisher's URL:	http://www.elsevier.com
Publisher's Address:	Amsterdam, The Netherlands	ISSN:	0747-7171

Vol, No, pp, Date

Volume*:	36	Number:	1-2
Publishing Date:	2003
Pages*:	217-233	Number of VG Pages:	17
Page Start:		Page End:
Sequence Number:		DOI:

Note, Abstract, ©

Note:
(LaTeX) Abstract:	When rewriting and completion techniques are used for equational theorem proving, the axiom set is saturated with the aim to get a rewrite system that is terminating and confluent on ground terms. To reduce the computational effort it should (1) be powerful for rewriting and (2) create not too many critical pairs. These problems become especially important if some operators are associative and commutative (\AC). We show in this paper how these two goals can be reached to some extent by using ground joinable equations for simplification purposes and omitting them from the generation of new facts. % For the special case of \AC-operators we present a simple redundancy criterion which is easy to implement, efficient, and effective in practice, leading to significant speed-ups.
URL for the Abstract:
Categories, Keywords:	Theorem Proving, Rewriting
HyperLinks / References / URLs:
Copyright Message:
Personal Comments:
Download Access Level:	Public

Correlation

MPG Unit:	Max-Planck-Institut für Informatik

MPG Subunit:	Programming Logics Group
Audience:	popular
Appearance:	MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort

BibTeX Entry:

@ARTICLE{AvenhausHillenbrandLoechner2003,
AUTHOR = {Avenhaus, J{\"u}rgen and Hillenbrand, Thomas and L{\"o}chner, Bernd},
TITLE = {On Using Ground Joinable Equations in Equational Theorem Proving},
JOURNAL = {Journal of Symbolic Computation},
PUBLISHER = {Elsevier},
YEAR = {2003},
NUMBER = {1-2},
VOLUME = {36},
PAGES = {217--233},
ADDRESS = {Amsterdam, The Netherlands},
ISBN = {0747-7171},
}

Entry last modified by Viorica Sofronie-Stokkermans, 03/12/2010

Edit History (please click the blue arrow to see the details)

	Editor(s) Thomas Hillenbrand	Created 04/07/2003 10:06:15 AM
Revisions 12. 11. 10. 9. 8.	Editor(s) Viorica Sofronie-Stokkermans Christine Kiesel Christine Kiesel Thomas Hillenbrand Thomas Hillenbrand	Edit Dates 06/23/2004 01:47:23 PM 17.06.2004 14:30:45 07.07.2003 16:34:29 07/02/2003 05:08:10 PM 13/06/2003 18:03:56

Attachment Section

gjoin.ps

gjoin.ps