English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  On Using Ground Joinable Equations in Equational Theorem Proving

Avenhaus, J., Hillenbrand, T., & Löchner, B. (2003). On Using Ground Joinable Equations in Equational Theorem Proving. Journal of Symbolic Computation, 36, 217-233.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DA8-E Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2DA9-C
Genre: Journal Article

Files

show Files
hide Files
:
gjoin.ps (Any fulltext), 264KB
 
File Permalink:
-
Name:
gjoin.ps
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/postscript
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Avenhaus, Jürgen, Author
Hillenbrand, Thomas1, 2, 3, Author           
Löchner, Bernd3, Author           
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
3Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2004-06-232003
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 201894
Other: Local-ID: C1256104005ECAFC-A129A5E170AD94F0C1256D01002C84B9-AvenhausHillenbrandLoechner2003
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Journal of Symbolic Computation
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 36 Sequence Number: - Start / End Page: 217 - 233 Identifier: ISSN: 0747-7171