I am interested in packaging nqthm, a public version of the Boyer-Moore
theorem prover. It is distributed under the GPL. However, it has the
export restriction quoted at the end. Is it possible to distribute it ?
If it is, should the interested users living in the listed countries be
informed of this restriction ? If yes, how ?
----------- quote ---------------------
Under U. S. law, Nqthm-1992 may be legally exported from the U. S. to
any country except as follows:
1. No trade is permitted with either Iraq or Yugoslavia except under
a special license, which would be very difficult to get.
2. Electronic transfer (e.g., FTP) to any of North Korea, Cuba, Haiti
or Libya is NOT permitted. Export on magnetic tape to these
countries IS permitted.
This export policy complies with a legal opinion rendered by
Computational Logic, Inc.'s attorneys in 1993.