Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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


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:




MPG Subunit:


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/20/2007
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)
Thomas Hillenbrand
Created
03/20/2007 10:17:16 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
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
gjoin.ps