- Injectivity of Composite Functions.
- Kim S. Larsen and Michael I. Schwartzbach.
Journal of Symbolic Computation, 17(5): 393-408, 1994.
The problem of deciding injectivity of functions is addressed. The functions
under consideration are compositions of more basic functions for which
information about injectivity properties is available. We present an algorithm
which will often be able to prove that such a composite function is injective.
This algorithm constructs a set of
propositional Horn clause axioms from the function
specification and the available information about the basic functions. The
existence of a proof of injectivity is then reduced to the problem of
propositional Horn clause deduction. Dowling and Gallier have designed several
very fast algorithms for this problem, the efficiency of which our algorithm
inherits. The proof of correctness of the algorithm amounts to showing
soundness and completeness of the generated Horn clause axioms.
- Link to the publication at the publisher's site - subscription may be required.
Text required by the publisher (if any):
The publication is available from ScienceDirect.
open access (156 KB)
The same as the publisher's version, when the publisher permits. Otherwise, the author's last version before the publisher's copyright; this is often exactly the same, but sometimes fonts, page numbers, figure numbers, etc. are different. It may also be a full version. However, it is safe to read this version, and at the same time cite the official version, as long as references to concrete locations, numbered theorems, etc. inside the article are avoided.
Other publications by the author.