Licensing Issues Regarding Automatic Reward Bounties

by Brown, Thursday, November 05, 2020, 19:10 (395 days ago)

My recent (second) proposal was to put automatic reward bounties on a specific collection of propositions translated from Mizar's MML and HOL4's library. A few days ago I thought about the possibility that there might be licensing issues with doing that. Here are the licenses I found for different systems/libraries:

Proofgold : MIT
MML: Dual License GPL and CC-BY-SA
HOL4: 3-clause BSD
HOL-light: 2-clause BSD
Coq: LGPL

The are all variants of open source, but none are the same. I'm neither a lawyer nor an expert on licensing. GPL (and LGPL?) are "copy-left" which runs the risk of creating a legal argument that Proofgold would need to become GPL if it included material from the MML (or Coq?). The BSD licenses seem more likely to be compatible with MIT, but, again, I'm not an expert. We plan to consult with an expert and get more information.

In principle I think none of this should apply since the Proofgold software would only be including *hashes* (Merkle roots) of propositions, not the propositions themselves, and no proofs from the other libraries at all. In practice I'm concerned that such an argument might have to be made in legal proceedings someday. If that's even a remote possibility, I'd recommend not using propositions from other libraries as part of Proofgold.

Of course, Proofgold is an open platform and there is no way to stop anyone from publishing material translated from other libraries. But including material directly into the software (even just hashes of the material) might open a can of worms.