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):
Waldmann, Uwedblp

BibTeX cite key*:

Waldmann2002bJSC

Title

Title*:

Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II)

Journal

Journal Title*:

Journal of Symbolic Computation
Journal's URL:

http://www.elsevier.com/locate/issn/0747-7171

Download URL
for the article:

http://www.idealibrary.com/links/doi/10.1006/jsco.2002.0537
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*:

33
Number:

6

Publishing Date:

June 2002

Pages*:

831-861
Number of
VG Pages:

62

Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

Cancellative superposition is a refutationally complete
calculus for first-order equational theorem proving in the
presence of the axioms of cancellative abelian monoids, and,
optionally, the torsion-freeness axioms. Thanks to strengthened
ordering restrictions, cancellative superposition avoids some
of the inefficiencies of classical AC-superposition calculi.
We show how the efficiency of cancellative superposition can
be further improved by using variable elimination techniques,
leading to a significant reduction of the number of variable
overlaps. In particular, we demonstrate that in divisible
torsion-free abelian groups, variable overlaps, AC-unification
and AC-orderings can be avoided completely.

URL for the Abstract:


Categories,
Keywords:

Theorem Proving, Superposition, Rewriting, Abelian Groups

HyperLinks / References / URLs:

http://www.mpi-sb.mpg.de/~uwe/paper/CAMRS-bibl.html

Copyright Message:


Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@ARTICLE{Waldmann2002bJSC,
AUTHOR = {Waldmann, Uwe},
 TITLE = {Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving ({Part II})},
 JOURNAL = {Journal of Symbolic Computation},
 PUBLISHER = {Elsevier},
 YEAR = {2002},
 NUMBER = {6},
 VOLUME = {33},
 PAGES = {831--861},
 ADDRESS = {Amsterdam, the Netherlands},
 MONTH = {June},
 ISBN = {0747-7171},
}

Entry last modified by Christine Kiesel, 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 Waldmann		Created
01/14/2003 05:39:48 PM
Revisions
6.
5.
4.
3.
2.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Uwe Brahm
Uwe Brahm		Edit Dates
29.07.2003 18:36:09
07.07.2003 15:43:35
07.07.2003 15:41:47
06/09/2003 01:57:58 AM
05/19/2003 01:29:06 PM