Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Formalizations Of Substitution Of Equals For Equals

Formalizations Of Substitution Of Equals For Equals

File(s)
98-1686.pdf (180.17 KB)
98-1686.ps (326.89 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7340
Collections
Computer Science Technical Reports
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
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1686
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance