Formalizations Of Substitution Of Equals For Equals
Permanent Link(s)
Collections
Author
Gries, David
Schneider, Fred B.
Abstract
Inference rule "substitution of equals for equals" has been formalized in terms of simple substitution (which performs a replacement even though a free occurrence of a variable is captured), contextual substitution (which prevents such capture), and function application. We show that in connection with pure first-order predicate calculus, the function-application and no-capture versions of the inference rule are the same and are weaker than the capture version. We discuss the deductive apparatus needed for the no-capture version to be as powerful as the capture version.
Date Issued
1998-05
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1686
Type
technical report