Access Restriction

Author Bachmair, Leo ♦ Ganzinger, Harald
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1998
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Chaining calculi ♦ Equational logic ♦ Reduction orderings ♦ Rewrite systems ♦ Term rewriting ♦ Transitive relations
Abstract We propose inference systems for binary relations that satisfy composition laws such as transitivity. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods as they are used in the context of resolution-type theorem proving. We establish the refutational completeness of these calculi and prove that our methods are compatible with the usual simplification techniques employed in refutational theorem provers, such as subsumption or tautology deletion. Various optimizations of the basic chaining calculus will be discussed for theories with equality and for total orderings. A key to the practicality of chaining methods is the extent to which so-called variable chaining can be avoided. We demonstrate that rewrite techniques considerably restrict variable chaining and that further restrictions are possible if the transitive relation under consideration satisfies additional properties, such as symmetry. But we also show that variable chaining cannot be completely avoided in general.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1998-11-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 45
Issue Number 6
Page Count 43
Starting Page 1007
Ending Page 1049

Open content in new tab

   Open content in new tab
Source: ACM Digital Library