Abstract
A new characterization of substitution, viz. as a universally conjunctive and universally disjunctive predicate transformer, is proposed. This characterization is also meaningful in point-free models for predicate calculus, and agrees with the classical definition of substitution whenever the latter is applicable.
Original language | English |
---|---|
Pages (from-to) | 205-214 |
Journal | Science of Computer Programming |
Volume | 27 |
Issue number | 2 |
DOIs | |
Publication status | Published - 1996 |