English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. Item Summary / 
  2. View item

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Rewrite Techniques for Transitive Relations

Bachmair, L., & Ganzinger, H. (1994). Rewrite Techniques for Transitive Relations. In Proceedings of the 9th IEEE Symposium on Logic in Computer Science (pp. 384-393). Los Alamitos, USA: IEEE.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD9E-A Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0014-AD9F-8
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Bachmair, Leo1, Author           
Ganzinger, Harald1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We propose inference systems for dealing with transitive relations in the context of resolution-type theorem proving. These inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods. We establish their refutational completeness and also prove their compatibility with the usual simplification techniques used in rewrite-based theorem provers. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. We demonstrate that rewrite techniques considerably restrict variable chaining, though we also show that they cannot be completely avoided for transitive relations in general. If the given relation satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss (partial) equivalence relations and congruence relations.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121994
 Publication Status: Issued
 Pages: -
 Publishing info: Los Alamitos, USA : IEEE
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519647
Other: Local-ID: C1256104005ECAFC-FC7CBADEDD415938C125614C004A73B2-BachmairGanzinger-94-lics
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Paris, France
Start-/End Date: 2003-07-08 - 2003-07-12

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 9th IEEE Symposium on Logic in Computer Science
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Los Alamitos, USA : IEEE
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 384 - 393 Identifier: -