forked from metamath/metamath-website-seed
-
Notifications
You must be signed in to change notification settings - Fork 0
/
copyright.html
307 lines (236 loc) · 11.1 KB
/
copyright.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML LANG="EN-US">
<HEAD>
<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<TITLE>Metamath Copyright Terms</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<STYLE TYPE="text/css">
<!--
/*hr {color:#FFBF72;background-color:#FFBF72;height:1px;border-style:none;}*/
-->
</STYLE>
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP><A HREF="../index.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Home"
TITLE="Metamath Home"
HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
</TD>
<TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Web Site - Copyright Terms</B> </FONT>
</TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP>
</TD>
</TR>
<TR>
<TD COLSPAN=3 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../mm.html">Mirrors</A> >
<A HREF="../index.html">Home</A> >
Copyright Terms
</FONT>
</TD>
</TR>
</TABLE>
<!--
<TABLE BORDER=0 WIDTH="100%"><TR>
<TD ALIGN=left VALIGN=middle WIDTH="25%"><FONT SIZE=-2
FACE=sans-serif><A HREF="index.html"><IMG SRC="mm.gif" BORDER=0
ALT="Home" HEIGHT=32 WIDTH=32 ALIGN=LEFT><IMG SRC="mpegif/spacer.gif" BORDER=0
ALT="" HEIGHT=32 WIDTH=2 ALIGN=LEFT>Metamath<BR>Home</A></FONT></TD>
<TD ALIGN=center NOWRAP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Web Site - Copyright Terms</B></FONT>
</TD>
<TD ALIGN=right VALIGN=top WIDTH="25%"> </TD>
</TR></TABLE>
-->
<HR NOSHADE SIZE=1>
<H3><A NAME="db"></A><FONT COLOR="#006633">Most Databases - Public
Domain</FONT></H3>
All Metamath databases (the *.mm files in the <A
HREF="index.html#mmprog">Metamath program download</A>, where "*"
matches any character string), except for the one mentioned below, are
waived of all rights, including copyright, according to the <A
HREF="http://creativecommons.org/publicdomain/zero/1.0/">CC0 Public
Domain Dedication</A> [accessed 17-Aug-2018]. A comment at the top
of each database indicates its copyright status.
<P><B>Exception.</B> The database file <A
HREF="metamath/peano.mm">peano.mm</A> (Peano arithmetic) is copyright by
Robert Solovay under the terms of the <A HREF="LICENSE.TXT">GNU General
Public License</A>.
<P><HR NOSHADE SIZE=1>
<H3><A NAME="sw"></A><FONT COLOR="#006633">Most Software -
GPL</FONT></H3>
<P>Unless otherwise stated, the software on this site (C, Java, and
Python programs) is copyright under the terms of the <A
HREF="LICENSE.TXT">GNU General Public License</A> Version 2 or later.
<P><B>Exception.</B> The <A HREF="index.html#eimm">eimm</A> program,
including its source code, is placed in the public domain.
<P><HR NOSHADE SIZE=1>
<H3><A NAME="web"></A><FONT COLOR="#006633">Some Web Pages - Open
Documentation Licenses</FONT></H3>
<P>If not otherwise stated on the pages themselves, the web pages on
this site are available under two licenses: <A
HREF="http://www.gnu.org/licenses/fdl.html">GNU Free Documentation
License</A> [accessed 17-Aug-2018] 1.2 or higher and the <A
HREF="http://creativecommons.org/licenses/by/2.5/">Creative Commons
Attribution License</A> [accessed 17-Aug-2018] 2.5 or higher. You may choose
whichever license you prefer.
<P><HR NOSHADE SIZE=1>
<H3><A NAME="pd"></A><FONT COLOR="#006633">Some Web Pages - Public
Domain</FONT></H3>
<P>Certain web pages, or parts of web pages, are placed in the public
domain by the author, Norman Megill, and other contributors if any, per
the <A HREF="http://creativecommons.org/publicdomain/zero/1.0/">CC0
Public Domain Dedication</A> [accessed 17-Aug-2018], when explicitly stated in a
notice at the bottom of the page.
<!--
, for example the
<A HREF="symbols/symbols.html">GIF and PNG Images for Math Symbols</A>
page and its image files.
-->
<P>The public domain release applies to the original content on those
pages, which (to the author's best knowledge and unless stated otherwise
in the notice at the bottom of the page) is all text and images
displayed on the page other than any short attributed quotations from
copyrighted sources.
<P>The public domain release applies worldwide. In case this is not
legally possible, the right is granted to use the work for any purpose,
without any conditions, unless such conditions are required by law.
<P><HR NOSHADE SIZE=1>
<H3><A NAME="logo"></A><FONT COLOR="#006633">Metamath Logo</FONT></H3>
In response to some inquiries, the image used for the Metamath logo is
specifically placed in the public domain. In other words, you are free
to sell coffee mugs or tee shirts with the logo without paying royalties
or acknowledging its source. Higher-resolution versions are available
as <A HREF="mmlogo.svg">mmlogo.svg</A> (courtesy of Giovanni Mascellani)
and <A HREF="mmlogo.gif">mmlogo.gif</A>. If you wish to credit the
image, "Credit: N. Megill (1994) and G. Mascellani (2019). Public
domain." is suggested. A logo with the Metamath name is <A
HREF="mmlogotitle.svg">mmlogotitle.svg</A> (courtesy of Giovanni
Mascellani).
<!--
<CENTER>
<IMG SRC="mmbig.gif"
ALT="Blazing aleph-null. Credit: N. Megill 1994. Public domain."
TITLE="Blazing aleph-null. Credit: N. Megill 1994. Public domain."
WIDTH=320 HEIGHT=320>
</CENTER>
-->
<P><HR NOSHADE SIZE=1>
<H3><A NAME="tm"></A><FONT COLOR="#006633">Trademarks</FONT></H3>
<P>Some web pages on this site may contain trademarked names or icons.
These belong to their respective owners.
<P>The name "Metamath" has been used publicly by Norman Megill since
1994 to refer to a computer language and related software.
<!--, and as such
is a de facto trademark that should not be claimed as a trademark by
another party.
-->
<!--
Otherwise, there are no restrictions on its use as a
generic (non-trademark) term.
-->
<P><HR NOSHADE SIZE=1>
<H3><A NAME="contrib"></A><FONT COLOR="#006633">Note for
Contributors</FONT></H3>
You are asked to place in the public domain any contribution you make to
the various databases, so that the databases can remain public-domain
documents. (If you wish to retain copyright to your work, you are free
to branch a public-domain database into a copyrighted work of your own.)
<P>Ordinarily, I will request that any patch or enhancement to a program
I have written be placed in the public domain, because eventually I may
place the program in the public domain. (If you wish to retain
copyright to your patch or enhancement, you are free to branch the
program into your own version with a compatible copyright license.)
<P><HR NOSHADE SIZE=1><CENTER><FONT SIZE=-1>(End of Copyright
Terms)</FONT></CENTER>
<P><HR NOSHADE SIZE=1>
<HR NOSHADE SIZE=1>
<CENTER>
<A NAME="editorial"></A>
<H2><FONT COLOR="#006633">Editorial Comment on Public Domain</FONT></H2>
</CENTER>
<P>After considering a number of copyright licensing alternatives, I
have concluded that for mathematical proofs, public domain is in the
best spirit and tradition of mathematics. This is a personal decision,
but I think that acknowledgment of my work is best dealt with through
courtesy and ethics rather than under threat of a lawsuit, which is what
a copyright license essentially entails. Plagiarizers will have their
own consciences (and reputations) to deal with, and I have more
important things to do with my time than to worry about them.
<P>Ultimately I can envision mathematical proof databases that will be
shared and built on, and there can be gray areas as to what constitutes
a copyright contribution. For example, if a proof is shortened or
rewritten completely, at what point does the original contributor's
"ownership" cease? Or proofs may be merged together, or a theorem may
be restated and reproved in a more convenient form, ideas or pieces of
one proof may be borrowed for use in another, and so on.
<P>A public domain proof database provides complete freedom from
distraction by such issues, allowing all effort to be focused on the
mathematics itself. Anyone can purge things, clean up comments, revise
theorems, and make use of it any way he or she sees fit without fear of
violating the fine print of a contract, license, or law. Professional
courtesy demands acknowledgment where appropriate and practical, but in
my view this should be a matter of ethics and common sense rather than
law.
<P>A mathematical result per se cannot be copyrighted, only its
presentation. The existing communication channels and peer-reviewed
journals already ensure proper credit for significant mathematical
discoveries, and journal publication establishing precedence will
usually happen well before formalization into a computer database. If,
in the distant future, computer-verified databases become a primary
means of communication, in principle they can be registered
<!-- <SUP>*</SUP> -->
with a trusted authority to establish precedence and still be placed in
the public domain. Public domain ensures that others are unencumbered to
freely build on the work and maximize the rate of progress in the field.
This is what already happens informally now. In present-day
mathematics, falsely claiming credit for someone else's discovery is an
ethical violation that is rarely pursued legally; instead, the
punishment that effectively results from a tarnished reputation is
already a severe one.
<P><A NAME="qed"></A>The founders of the <A
HREF="http://mizar.org/qed/">QED Project</A> [accessed 17-Aug-2018] also
considered public domain important for its purposes. The goal of this
project is to build a comprehensive repository of computer-verified
mathematics. From the <A
HREF="http://www.rbjones.com/rbjpub/logic/qedres02.htm">QED
Manifesto</A> [accessed 17-Aug-2018]:
<BLOCKQUOTE>
Objection 2: Intellectual property problems. Such an enterprise as QED
is doomed because as soon as it is even slightly successful, it will be
so swamped by lawyers with issues of ownership, copyright, trade
secrecy, and patent law that the necessary wide cooperation of hundreds
of mathematicians, computer scientists, research agencies, and
institutions will become impossible.
<P>Reply to Objection 2: In full cognizance of the dangers of this
objection, we put forward as a fundamental and initial principle that
the entirety of the QED system is to be in the international public
domain, so that all can freely benefit from it, and thus be inspired to
contribute to its further development.
</BLOCKQUOTE>
<P><HR NOSHADE SIZE=1>
<A
HREF="http://validator.w3.org/check/referer"><IMG BORDER="0"
SRC="valid-html401.png" ALT="Valid HTML 4.01!" HEIGHT="31"
WIDTH="88" ALIGN=right></A>
<CENTER><I><FONT SIZE=-1>This page was last updated on
5-Jun-2019.</FONT></I></CENTER>
<CENTER><FONT FACE="ARIAL" SIZE=-2>Your
comments are welcome: <A HREF="email.html">contact us</A></FONT></CENTER>
<!-- <SCRIPT SRC="http://www.google-analytics.com/urchin.js" TYPE="text/javascript">
</SCRIPT>
<SCRIPT TYPE="text/javascript">
_uacct = "UA-1862729-1";
urchinTracker();
</SCRIPT>
-->
</BODY>
</HTML>