mirror of
https://github.com/RAIRLab/Spectra.git
synced 2025-02-15 17:51:04 +00:00
Moved snark to submodule
This commit is contained in:
parent
0b01117377
commit
4f1f9c0b83
239 changed files with 6 additions and 36288 deletions
3
.gitmodules
vendored
Normal file
3
.gitmodules
vendored
Normal file
|
@ -0,0 +1,3 @@
|
|||
[submodule "snark"]
|
||||
path = snark
|
||||
url = https://github.com/RAIRLab/snark
|
|
@ -1,6 +1,6 @@
|
|||
FROM maven:3.6.3-jdk-11
|
||||
ADD ./target/server-jar-with-dependencies.jar ./
|
||||
RUN mkdir -p ./snark-20120808r02
|
||||
COPY ./snark-20120808r02/ ./snark-20120808r02
|
||||
RUN mkdir -p ./snark
|
||||
COPY ./snark/ ./snark2
|
||||
EXPOSE 25333 25334
|
||||
CMD java -jar server-jar-with-dependencies.jar
|
1
snark
Submodule
1
snark
Submodule
|
@ -0,0 +1 @@
|
|||
Subproject commit 1b657eadf4e87f3ba46e030c3e549854b2454a4e
|
|
@ -1,53 +0,0 @@
|
|||
SNARK is run regularly in
|
||||
Macintosh Common Lisp on Mac OS X
|
||||
Steel Bank Common Lisp (SBCL) on Mac OS X
|
||||
Clozure Common Lisp (CCL nee OpenMCL) on Mac OS X
|
||||
and has been run in other ANSI Common Lisp systems
|
||||
|
||||
After editing for the correct name and location of the SBCL Lisp system in the appropriate make-xxx file
|
||||
a 32-bit executable of SNARK in SBCL named snark can be made by ./make-snark-sbcl;
|
||||
a 64-bit executable of SNARK in SBCL named snark64 can be make by ./make-snark-sbcl64.
|
||||
|
||||
After editing for the correct name and location of the CCL Lisp system in the appropriate make-xxx file
|
||||
a 32-bit executable of SNARK in CCL named snark-ccl can be made by ./make-snark-ccl;
|
||||
a 64-bit executable of SNARK in CCL named snark-ccl64 can be maded by ./make-snark-ccl64
|
||||
|
||||
|
||||
|
||||
Older detailed instructions:
|
||||
|
||||
(replace "yyyymmdd" by the SNARK version date)
|
||||
|
||||
Installing SNARK:
|
||||
|
||||
tar xfz snark-yyyymmdd.tar.gz
|
||||
cd snark-yyyymmdd
|
||||
lisp
|
||||
(load "snark-system.lisp")
|
||||
(make-snark-system t) ;t specifies compilation
|
||||
(make-snark-system t) ;compile again for more inlining (optional)
|
||||
;can use :optimize instead of t to compile for
|
||||
;higher speed at the expense of less error checking
|
||||
(quit)
|
||||
|
||||
Running SNARK:
|
||||
|
||||
lisp
|
||||
(load "snark-system.lisp")
|
||||
(make-snark-system) ;loads SNARK files compiled above
|
||||
:
|
||||
|
||||
The lengthy load process in running SNARK can be eliminated
|
||||
for CCL, SBCL, CMUCL, Allegro Common Lisp, or CLISP by doing
|
||||
lisp
|
||||
(load "snark-system.lisp")
|
||||
(make-snark-system)
|
||||
(save-snark-system)
|
||||
after installing SNARK as above.
|
||||
(save-snark-system) will print instructions for running
|
||||
the resulting Lisp core image with SNARK preloaded.
|
||||
|
||||
In the case of SBCL, (save-snark-system) can be replaced by
|
||||
(save-snark-system :name "snark" :executable t)
|
||||
to create a standalone SNARK executable. This is done
|
||||
by the make-snark-sbcl and make-snark-sbcl64 scripts.
|
|
@ -1,453 +0,0 @@
|
|||
MOZILLA PUBLIC LICENSE
|
||||
Version 1.1
|
||||
|
||||
---------------
|
||||
|
||||
1. Definitions.
|
||||
|
||||
1.0.1. "Commercial Use" means distribution or otherwise making the
|
||||
Covered Code available to a third party.
|
||||
|
||||
1.1. "Contributor" means each entity that creates or contributes to
|
||||
the creation of Modifications.
|
||||
|
||||
1.2. "Contributor Version" means the combination of the Original
|
||||
Code, prior Modifications used by a Contributor, and the Modifications
|
||||
made by that particular Contributor.
|
||||
|
||||
1.3. "Covered Code" means the Original Code or Modifications or the
|
||||
combination of the Original Code and Modifications, in each case
|
||||
including portions thereof.
|
||||
|
||||
1.4. "Electronic Distribution Mechanism" means a mechanism generally
|
||||
accepted in the software development community for the electronic
|
||||
transfer of data.
|
||||
|
||||
1.5. "Executable" means Covered Code in any form other than Source
|
||||
Code.
|
||||
|
||||
1.6. "Initial Developer" means the individual or entity identified
|
||||
as the Initial Developer in the Source Code notice required by Exhibit
|
||||
A.
|
||||
|
||||
1.7. "Larger Work" means a work which combines Covered Code or
|
||||
portions thereof with code not governed by the terms of this License.
|
||||
|
||||
1.8. "License" means this document.
|
||||
|
||||
1.8.1. "Licensable" means having the right to grant, to the maximum
|
||||
extent possible, whether at the time of the initial grant or
|
||||
subsequently acquired, any and all of the rights conveyed herein.
|
||||
|
||||
1.9. "Modifications" means any addition to or deletion from the
|
||||
substance or structure of either the Original Code or any previous
|
||||
Modifications. When Covered Code is released as a series of files, a
|
||||
Modification is:
|
||||
A. Any addition to or deletion from the contents of a file
|
||||
containing Original Code or previous Modifications.
|
||||
|
||||
B. Any new file that contains any part of the Original Code or
|
||||
previous Modifications.
|
||||
|
||||
1.10. "Original Code" means Source Code of computer software code
|
||||
which is described in the Source Code notice required by Exhibit A as
|
||||
Original Code, and which, at the time of its release under this
|
||||
License is not already Covered Code governed by this License.
|
||||
|
||||
1.10.1. "Patent Claims" means any patent claim(s), now owned or
|
||||
hereafter acquired, including without limitation, method, process,
|
||||
and apparatus claims, in any patent Licensable by grantor.
|
||||
|
||||
1.11. "Source Code" means the preferred form of the Covered Code for
|
||||
making modifications to it, including all modules it contains, plus
|
||||
any associated interface definition files, scripts used to control
|
||||
compilation and installation of an Executable, or source code
|
||||
differential comparisons against either the Original Code or another
|
||||
well known, available Covered Code of the Contributor's choice. The
|
||||
Source Code can be in a compressed or archival form, provided the
|
||||
appropriate decompression or de-archiving software is widely available
|
||||
for no charge.
|
||||
|
||||
1.12. "You" (or "Your") means an individual or a legal entity
|
||||
exercising rights under, and complying with all of the terms of, this
|
||||
License or a future version of this License issued under Section 6.1.
|
||||
For legal entities, "You" includes any entity which controls, is
|
||||
controlled by, or is under common control with You. For purposes of
|
||||
this definition, "control" means (a) the power, direct or indirect,
|
||||
to cause the direction or management of such entity, whether by
|
||||
contract or otherwise, or (b) ownership of more than fifty percent
|
||||
(50%) of the outstanding shares or beneficial ownership of such
|
||||
entity.
|
||||
|
||||
2. Source Code License.
|
||||
|
||||
2.1. The Initial Developer Grant.
|
||||
The Initial Developer hereby grants You a world-wide, royalty-free,
|
||||
non-exclusive license, subject to third party intellectual property
|
||||
claims:
|
||||
(a) under intellectual property rights (other than patent or
|
||||
trademark) Licensable by Initial Developer to use, reproduce,
|
||||
modify, display, perform, sublicense and distribute the Original
|
||||
Code (or portions thereof) with or without Modifications, and/or
|
||||
as part of a Larger Work; and
|
||||
|
||||
(b) under Patents Claims infringed by the making, using or
|
||||
selling of Original Code, to make, have made, use, practice,
|
||||
sell, and offer for sale, and/or otherwise dispose of the
|
||||
Original Code (or portions thereof).
|
||||
|
||||
(c) the licenses granted in this Section 2.1(a) and (b) are
|
||||
effective on the date Initial Developer first distributes
|
||||
Original Code under the terms of this License.
|
||||
|
||||
(d) Notwithstanding Section 2.1(b) above, no patent license is
|
||||
granted: 1) for code that You delete from the Original Code; 2)
|
||||
separate from the Original Code; or 3) for infringements caused
|
||||
by: i) the modification of the Original Code or ii) the
|
||||
combination of the Original Code with other software or devices.
|
||||
|
||||
2.2. Contributor Grant.
|
||||
Subject to third party intellectual property claims, each Contributor
|
||||
hereby grants You a world-wide, royalty-free, non-exclusive license
|
||||
|
||||
(a) under intellectual property rights (other than patent or
|
||||
trademark) Licensable by Contributor, to use, reproduce, modify,
|
||||
display, perform, sublicense and distribute the Modifications
|
||||
created by such Contributor (or portions thereof) either on an
|
||||
unmodified basis, with other Modifications, as Covered Code
|
||||
and/or as part of a Larger Work; and
|
||||
|
||||
(b) under Patent Claims infringed by the making, using, or
|
||||
selling of Modifications made by that Contributor either alone
|
||||
and/or in combination with its Contributor Version (or portions
|
||||
of such combination), to make, use, sell, offer for sale, have
|
||||
made, and/or otherwise dispose of: 1) Modifications made by that
|
||||
Contributor (or portions thereof); and 2) the combination of
|
||||
Modifications made by that Contributor with its Contributor
|
||||
Version (or portions of such combination).
|
||||
|
||||
(c) the licenses granted in Sections 2.2(a) and 2.2(b) are
|
||||
effective on the date Contributor first makes Commercial Use of
|
||||
the Covered Code.
|
||||
|
||||
(d) Notwithstanding Section 2.2(b) above, no patent license is
|
||||
granted: 1) for any code that Contributor has deleted from the
|
||||
Contributor Version; 2) separate from the Contributor Version;
|
||||
3) for infringements caused by: i) third party modifications of
|
||||
Contributor Version or ii) the combination of Modifications made
|
||||
by that Contributor with other software (except as part of the
|
||||
Contributor Version) or other devices; or 4) under Patent Claims
|
||||
infringed by Covered Code in the absence of Modifications made by
|
||||
that Contributor.
|
||||
|
||||
3. Distribution Obligations.
|
||||
|
||||
3.1. Application of License.
|
||||
The Modifications which You create or to which You contribute are
|
||||
governed by the terms of this License, including without limitation
|
||||
Section 2.2. The Source Code version of Covered Code may be
|
||||
distributed only under the terms of this License or a future version
|
||||
of this License released under Section 6.1, and You must include a
|
||||
copy of this License with every copy of the Source Code You
|
||||
distribute. You may not offer or impose any terms on any Source Code
|
||||
version that alters or restricts the applicable version of this
|
||||
License or the recipients' rights hereunder. However, You may include
|
||||
an additional document offering the additional rights described in
|
||||
Section 3.5.
|
||||
|
||||
3.2. Availability of Source Code.
|
||||
Any Modification which You create or to which You contribute must be
|
||||
made available in Source Code form under the terms of this License
|
||||
either on the same media as an Executable version or via an accepted
|
||||
Electronic Distribution Mechanism to anyone to whom you made an
|
||||
Executable version available; and if made available via Electronic
|
||||
Distribution Mechanism, must remain available for at least twelve (12)
|
||||
months after the date it initially became available, or at least six
|
||||
(6) months after a subsequent version of that particular Modification
|
||||
has been made available to such recipients. You are responsible for
|
||||
ensuring that the Source Code version remains available even if the
|
||||
Electronic Distribution Mechanism is maintained by a third party.
|
||||
|
||||
3.3. Description of Modifications.
|
||||
You must cause all Covered Code to which You contribute to contain a
|
||||
file documenting the changes You made to create that Covered Code and
|
||||
the date of any change. You must include a prominent statement that
|
||||
the Modification is derived, directly or indirectly, from Original
|
||||
Code provided by the Initial Developer and including the name of the
|
||||
Initial Developer in (a) the Source Code, and (b) in any notice in an
|
||||
Executable version or related documentation in which You describe the
|
||||
origin or ownership of the Covered Code.
|
||||
|
||||
3.4. Intellectual Property Matters
|
||||
(a) Third Party Claims.
|
||||
If Contributor has knowledge that a license under a third party's
|
||||
intellectual property rights is required to exercise the rights
|
||||
granted by such Contributor under Sections 2.1 or 2.2,
|
||||
Contributor must include a text file with the Source Code
|
||||
distribution titled "LEGAL" which describes the claim and the
|
||||
party making the claim in sufficient detail that a recipient will
|
||||
know whom to contact. If Contributor obtains such knowledge after
|
||||
the Modification is made available as described in Section 3.2,
|
||||
Contributor shall promptly modify the LEGAL file in all copies
|
||||
Contributor makes available thereafter and shall take other steps
|
||||
(such as notifying appropriate mailing lists or newsgroups)
|
||||
reasonably calculated to inform those who received the Covered
|
||||
Code that new knowledge has been obtained.
|
||||
|
||||
(b) Contributor APIs.
|
||||
If Contributor's Modifications include an application programming
|
||||
interface and Contributor has knowledge of patent licenses which
|
||||
are reasonably necessary to implement that API, Contributor must
|
||||
also include this information in the LEGAL file.
|
||||
|
||||
(c) Representations.
|
||||
Contributor represents that, except as disclosed pursuant to
|
||||
Section 3.4(a) above, Contributor believes that Contributor's
|
||||
Modifications are Contributor's original creation(s) and/or
|
||||
Contributor has sufficient rights to grant the rights conveyed by
|
||||
this License.
|
||||
|
||||
3.5. Required Notices.
|
||||
You must duplicate the notice in Exhibit A in each file of the Source
|
||||
Code. If it is not possible to put such notice in a particular Source
|
||||
Code file due to its structure, then You must include such notice in a
|
||||
location (such as a relevant directory) where a user would be likely
|
||||
to look for such a notice. If You created one or more Modification(s)
|
||||
You may add your name as a Contributor to the notice described in
|
||||
Exhibit A. You must also duplicate this License in any documentation
|
||||
for the Source Code where You describe recipients' rights or ownership
|
||||
rights relating to Covered Code. You may choose to offer, and to
|
||||
charge a fee for, warranty, support, indemnity or liability
|
||||
obligations to one or more recipients of Covered Code. However, You
|
||||
may do so only on Your own behalf, and not on behalf of the Initial
|
||||
Developer or any Contributor. You must make it absolutely clear than
|
||||
any such warranty, support, indemnity or liability obligation is
|
||||
offered by You alone, and You hereby agree to indemnify the Initial
|
||||
Developer and every Contributor for any liability incurred by the
|
||||
Initial Developer or such Contributor as a result of warranty,
|
||||
support, indemnity or liability terms You offer.
|
||||
|
||||
3.6. Distribution of Executable Versions.
|
||||
You may distribute Covered Code in Executable form only if the
|
||||
requirements of Section 3.1-3.5 have been met for that Covered Code,
|
||||
and if You include a notice stating that the Source Code version of
|
||||
the Covered Code is available under the terms of this License,
|
||||
including a description of how and where You have fulfilled the
|
||||
obligations of Section 3.2. The notice must be conspicuously included
|
||||
in any notice in an Executable version, related documentation or
|
||||
collateral in which You describe recipients' rights relating to the
|
||||
Covered Code. You may distribute the Executable version of Covered
|
||||
Code or ownership rights under a license of Your choice, which may
|
||||
contain terms different from this License, provided that You are in
|
||||
compliance with the terms of this License and that the license for the
|
||||
Executable version does not attempt to limit or alter the recipient's
|
||||
rights in the Source Code version from the rights set forth in this
|
||||
License. If You distribute the Executable version under a different
|
||||
license You must make it absolutely clear that any terms which differ
|
||||
from this License are offered by You alone, not by the Initial
|
||||
Developer or any Contributor. You hereby agree to indemnify the
|
||||
Initial Developer and every Contributor for any liability incurred by
|
||||
the Initial Developer or such Contributor as a result of any such
|
||||
terms You offer.
|
||||
|
||||
3.7. Larger Works.
|
||||
You may create a Larger Work by combining Covered Code with other code
|
||||
not governed by the terms of this License and distribute the Larger
|
||||
Work as a single product. In such a case, You must make sure the
|
||||
requirements of this License are fulfilled for the Covered Code.
|
||||
|
||||
4. Inability to Comply Due to Statute or Regulation.
|
||||
|
||||
If it is impossible for You to comply with any of the terms of this
|
||||
License with respect to some or all of the Covered Code due to
|
||||
statute, judicial order, or regulation then You must: (a) comply with
|
||||
the terms of this License to the maximum extent possible; and (b)
|
||||
describe the limitations and the code they affect. Such description
|
||||
must be included in the LEGAL file described in Section 3.4 and must
|
||||
be included with all distributions of the Source Code. Except to the
|
||||
extent prohibited by statute or regulation, such description must be
|
||||
sufficiently detailed for a recipient of ordinary skill to be able to
|
||||
understand it.
|
||||
|
||||
5. Application of this License.
|
||||
|
||||
This License applies to code to which the Initial Developer has
|
||||
attached the notice in Exhibit A and to related Covered Code.
|
||||
|
||||
6. Versions of the License.
|
||||
|
||||
6.1. New Versions.
|
||||
Netscape Communications Corporation ("Netscape") may publish revised
|
||||
and/or new versions of the License from time to time. Each version
|
||||
will be given a distinguishing version number.
|
||||
|
||||
6.2. Effect of New Versions.
|
||||
Once Covered Code has been published under a particular version of the
|
||||
License, You may always continue to use it under the terms of that
|
||||
version. You may also choose to use such Covered Code under the terms
|
||||
of any subsequent version of the License published by Netscape. No one
|
||||
other than Netscape has the right to modify the terms applicable to
|
||||
Covered Code created under this License.
|
||||
|
||||
6.3. Derivative Works.
|
||||
If You create or use a modified version of this License (which you may
|
||||
only do in order to apply it to code which is not already Covered Code
|
||||
governed by this License), You must (a) rename Your license so that
|
||||
the phrases "Mozilla", "MOZILLAPL", "MOZPL", "Netscape",
|
||||
"MPL", "NPL" or any confusingly similar phrase do not appear in your
|
||||
license (except to note that your license differs from this License)
|
||||
and (b) otherwise make it clear that Your version of the license
|
||||
contains terms which differ from the Mozilla Public License and
|
||||
Netscape Public License. (Filling in the name of the Initial
|
||||
Developer, Original Code or Contributor in the notice described in
|
||||
Exhibit A shall not of themselves be deemed to be modifications of
|
||||
this License.)
|
||||
|
||||
7. DISCLAIMER OF WARRANTY.
|
||||
|
||||
COVERED CODE IS PROVIDED UNDER THIS LICENSE ON AN "AS IS" BASIS,
|
||||
WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING,
|
||||
WITHOUT LIMITATION, WARRANTIES THAT THE COVERED CODE IS FREE OF
|
||||
DEFECTS, MERCHANTABLE, FIT FOR A PARTICULAR PURPOSE OR NON-INFRINGING.
|
||||
THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE COVERED CODE
|
||||
IS WITH YOU. SHOULD ANY COVERED CODE PROVE DEFECTIVE IN ANY RESPECT,
|
||||
YOU (NOT THE INITIAL DEVELOPER OR ANY OTHER CONTRIBUTOR) ASSUME THE
|
||||
COST OF ANY NECESSARY SERVICING, REPAIR OR CORRECTION. THIS DISCLAIMER
|
||||
OF WARRANTY CONSTITUTES AN ESSENTIAL PART OF THIS LICENSE. NO USE OF
|
||||
ANY COVERED CODE IS AUTHORIZED HEREUNDER EXCEPT UNDER THIS DISCLAIMER.
|
||||
|
||||
8. TERMINATION.
|
||||
|
||||
8.1. This License and the rights granted hereunder will terminate
|
||||
automatically if You fail to comply with terms herein and fail to cure
|
||||
such breach within 30 days of becoming aware of the breach. All
|
||||
sublicenses to the Covered Code which are properly granted shall
|
||||
survive any termination of this License. Provisions which, by their
|
||||
nature, must remain in effect beyond the termination of this License
|
||||
shall survive.
|
||||
|
||||
8.2. If You initiate litigation by asserting a patent infringement
|
||||
claim (excluding declatory judgment actions) against Initial Developer
|
||||
or a Contributor (the Initial Developer or Contributor against whom
|
||||
You file such action is referred to as "Participant") alleging that:
|
||||
|
||||
(a) such Participant's Contributor Version directly or indirectly
|
||||
infringes any patent, then any and all rights granted by such
|
||||
Participant to You under Sections 2.1 and/or 2.2 of this License
|
||||
shall, upon 60 days notice from Participant terminate prospectively,
|
||||
unless if within 60 days after receipt of notice You either: (i)
|
||||
agree in writing to pay Participant a mutually agreeable reasonable
|
||||
royalty for Your past and future use of Modifications made by such
|
||||
Participant, or (ii) withdraw Your litigation claim with respect to
|
||||
the Contributor Version against such Participant. If within 60 days
|
||||
of notice, a reasonable royalty and payment arrangement are not
|
||||
mutually agreed upon in writing by the parties or the litigation claim
|
||||
is not withdrawn, the rights granted by Participant to You under
|
||||
Sections 2.1 and/or 2.2 automatically terminate at the expiration of
|
||||
the 60 day notice period specified above.
|
||||
|
||||
(b) any software, hardware, or device, other than such Participant's
|
||||
Contributor Version, directly or indirectly infringes any patent, then
|
||||
any rights granted to You by such Participant under Sections 2.1(b)
|
||||
and 2.2(b) are revoked effective as of the date You first made, used,
|
||||
sold, distributed, or had made, Modifications made by that
|
||||
Participant.
|
||||
|
||||
8.3. If You assert a patent infringement claim against Participant
|
||||
alleging that such Participant's Contributor Version directly or
|
||||
indirectly infringes any patent where such claim is resolved (such as
|
||||
by license or settlement) prior to the initiation of patent
|
||||
infringement litigation, then the reasonable value of the licenses
|
||||
granted by such Participant under Sections 2.1 or 2.2 shall be taken
|
||||
into account in determining the amount or value of any payment or
|
||||
license.
|
||||
|
||||
8.4. In the event of termination under Sections 8.1 or 8.2 above,
|
||||
all end user license agreements (excluding distributors and resellers)
|
||||
which have been validly granted by You or any distributor hereunder
|
||||
prior to termination shall survive termination.
|
||||
|
||||
9. LIMITATION OF LIABILITY.
|
||||
|
||||
UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL THEORY, WHETHER TORT
|
||||
(INCLUDING NEGLIGENCE), CONTRACT, OR OTHERWISE, SHALL YOU, THE INITIAL
|
||||
DEVELOPER, ANY OTHER CONTRIBUTOR, OR ANY DISTRIBUTOR OF COVERED CODE,
|
||||
OR ANY SUPPLIER OF ANY OF SUCH PARTIES, BE LIABLE TO ANY PERSON FOR
|
||||
ANY INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES OF ANY
|
||||
CHARACTER INCLUDING, WITHOUT LIMITATION, DAMAGES FOR LOSS OF GOODWILL,
|
||||
WORK STOPPAGE, COMPUTER FAILURE OR MALFUNCTION, OR ANY AND ALL OTHER
|
||||
COMMERCIAL DAMAGES OR LOSSES, EVEN IF SUCH PARTY SHALL HAVE BEEN
|
||||
INFORMED OF THE POSSIBILITY OF SUCH DAMAGES. THIS LIMITATION OF
|
||||
LIABILITY SHALL NOT APPLY TO LIABILITY FOR DEATH OR PERSONAL INJURY
|
||||
RESULTING FROM SUCH PARTY'S NEGLIGENCE TO THE EXTENT APPLICABLE LAW
|
||||
PROHIBITS SUCH LIMITATION. SOME JURISDICTIONS DO NOT ALLOW THE
|
||||
EXCLUSION OR LIMITATION OF INCIDENTAL OR CONSEQUENTIAL DAMAGES, SO
|
||||
THIS EXCLUSION AND LIMITATION MAY NOT APPLY TO YOU.
|
||||
|
||||
10. U.S. GOVERNMENT END USERS.
|
||||
|
||||
The Covered Code is a "commercial item," as that term is defined in
|
||||
48 C.F.R. 2.101 (Oct. 1995), consisting of "commercial computer
|
||||
software" and "commercial computer software documentation," as such
|
||||
terms are used in 48 C.F.R. 12.212 (Sept. 1995). Consistent with 48
|
||||
C.F.R. 12.212 and 48 C.F.R. 227.7202-1 through 227.7202-4 (June 1995),
|
||||
all U.S. Government End Users acquire Covered Code with only those
|
||||
rights set forth herein.
|
||||
|
||||
11. MISCELLANEOUS.
|
||||
|
||||
This License represents the complete agreement concerning subject
|
||||
matter hereof. If any provision of this License is held to be
|
||||
unenforceable, such provision shall be reformed only to the extent
|
||||
necessary to make it enforceable. This License shall be governed by
|
||||
California law provisions (except to the extent applicable law, if
|
||||
any, provides otherwise), excluding its conflict-of-law provisions.
|
||||
With respect to disputes in which at least one party is a citizen of,
|
||||
or an entity chartered or registered to do business in the United
|
||||
States of America, any litigation relating to this License shall be
|
||||
subject to the jurisdiction of the Federal Courts of the Northern
|
||||
District of California, with venue lying in Santa Clara County,
|
||||
California, with the losing party responsible for costs, including
|
||||
without limitation, court costs and reasonable attorneys' fees and
|
||||
expenses. The application of the United Nations Convention on
|
||||
Contracts for the International Sale of Goods is expressly excluded.
|
||||
Any law or regulation which provides that the language of a contract
|
||||
shall be construed against the drafter shall not apply to this
|
||||
License.
|
||||
|
||||
12. RESPONSIBILITY FOR CLAIMS.
|
||||
|
||||
As between Initial Developer and the Contributors, each party is
|
||||
responsible for claims and damages arising, directly or indirectly,
|
||||
out of its utilization of rights under this License and You agree to
|
||||
work with Initial Developer and Contributors to distribute such
|
||||
responsibility on an equitable basis. Nothing herein is intended or
|
||||
shall be deemed to constitute any admission of liability.
|
||||
|
||||
13. MULTIPLE-LICENSED CODE.
|
||||
|
||||
Initial Developer may designate portions of the Covered Code as
|
||||
"Multiple-Licensed". "Multiple-Licensed" means that the Initial
|
||||
Developer permits you to utilize portions of the Covered Code under
|
||||
Your choice of the NPL or the alternative licenses, if any, specified
|
||||
by the Initial Developer in the file described in Exhibit A.
|
||||
|
||||
EXHIBIT A -Mozilla Public License.
|
||||
|
||||
``The contents of this file are subject to the Mozilla Public License
|
||||
Version 1.1 (the "License"); you may not use this file except in
|
||||
compliance with the License. You may obtain a copy of the License at
|
||||
http://www.mozilla.org/MPL/
|
||||
|
||||
Software distributed under the License is distributed on an "AS IS"
|
||||
basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
|
||||
License for the specific language governing rights and limitations
|
||||
under the License.
|
||||
|
||||
The Original Code is SNARK.
|
||||
|
||||
The Initial Developer of the Original Code is SRI International.
|
||||
Portions created by the Initial Developer are Copyright (C) 1981-2011.
|
||||
All Rights Reserved.
|
||||
|
||||
Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.
|
|
@ -1,36 +0,0 @@
|
|||
(replace "yyyymmdd" by the SNARK version date)
|
||||
|
||||
Obtaining SNARK:
|
||||
|
||||
SNARK can be downloaded from the SNARK web page
|
||||
http://www.ai.sri.com/~stickel/snark.html
|
||||
|
||||
See INSTALL file for installation instructions
|
||||
|
||||
Running SNARK:
|
||||
|
||||
lisp
|
||||
(load "snark-system.lisp")
|
||||
(make-snark-system)
|
||||
:
|
||||
|
||||
Examples:
|
||||
|
||||
(overbeek-test) in overbeek-test.lisp
|
||||
some standard theorem-proving examples, some time-consuming
|
||||
|
||||
(steamroller-example) in steamroller-example.lisp
|
||||
illustrates sorts
|
||||
|
||||
(front-last-example) in front-last-example.lisp
|
||||
illustrates program synthesis
|
||||
|
||||
(reverse-example) in reverse-example.lisp
|
||||
illustrates logic programming style usage
|
||||
|
||||
A guide to SNARK has been written:
|
||||
|
||||
http://www.ai.sri.com/snark/tutorial/tutorial.html
|
||||
|
||||
but has not been updated yet to reflect changes in SNARK,
|
||||
especially for temporal and spatial reasoning.
|
|
@ -1,4 +0,0 @@
|
|||
(load "snark-system.lisp")
|
||||
(make-snark-system t)
|
||||
(make-snark-system :optimize)
|
||||
(quit)
|
|
@ -1,47 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : BOO002-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Boolean Algebra (Ternary)
|
||||
; Problem : In B3 algebra, X * X^-1 * Y = Y
|
||||
; Version : [OTTER] (equality) axioms : Reduced > Incomplete.
|
||||
; English :
|
||||
|
||||
; Refs : [LO85] Lusk & Overbeek (1985), Reasoning about Equality
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [Ove90]
|
||||
; Names : Problem 5 [LO85]
|
||||
; : CADE-11 Competition Eq-3 [Ove90]
|
||||
; : THEOREM EQ-3 [LM93]
|
||||
; : PROBLEM 3 [Zha93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.33 v2.2.0, 0.43 v2.1.0, 0.38 v2.0.0
|
||||
; Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 1 RR)
|
||||
; Number of literals : 5 ( 5 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 4 ( 2 constant; 0-3 arity)
|
||||
; Number of variables : 11 ( 2 singleton)
|
||||
; Maximal term depth : 3 ( 2 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp BOO002-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; associativity, axiom.
|
||||
(or (= (multiply (multiply ?A ?B ?C) ?D (multiply ?A ?B ?E)) (multiply ?A ?B (multiply ?C ?D ?E))))
|
||||
|
||||
; ternary_multiply_1, axiom.
|
||||
(or (= (multiply ?A ?B ?B) ?B))
|
||||
|
||||
; ternary_multiply_2, axiom.
|
||||
(or (= (multiply ?A ?A ?B) ?A))
|
||||
|
||||
; left_inverse, axiom.
|
||||
(or (= (multiply (inverse ?A) ?A ?B) ?B))
|
||||
|
||||
; prove_equation, conjecture.
|
||||
(or (/= (multiply a (inverse a) b) b))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,53 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : COL003-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Combinatory Logic
|
||||
; Problem : Strong fixed point for B and W
|
||||
; Version : [WM88] (equality) axioms.
|
||||
; English : The strong fixed point property holds for the set
|
||||
; P consisting of the combinators B and W alone, where ((Bx)y)z
|
||||
; = x(yz) and (Wx)y = (xy)y.
|
||||
|
||||
; Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi
|
||||
; : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem
|
||||
; : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq
|
||||
; : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit
|
||||
; : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [WM88]
|
||||
; Names : C2 [WM88]
|
||||
; : Test Problem 17 [Wos88]
|
||||
; : Sages and Combinatory Logic [Wos88]
|
||||
; : CADE-11 Competition Eq-8 [Ove90]
|
||||
; : CL2 [LW92]
|
||||
; : THEOREM EQ-8 [LM93]
|
||||
; : Question 3 [Wos93]
|
||||
; : Question 5 [Wos93]
|
||||
; : PROBLEM 8 [Zha93]
|
||||
|
||||
; Status : unknown
|
||||
; Rating : 1.00 v2.0.0
|
||||
; Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 1 RR)
|
||||
; Number of literals : 3 ( 3 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 4 ( 2 constant; 0-2 arity)
|
||||
; Number of variables : 6 ( 0 singleton)
|
||||
; Maximal term depth : 4 ( 3 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp COL003-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; b_definition, axiom.
|
||||
(or (= (apply (apply (apply b ?A) ?B) ?C) (apply ?A (apply ?B ?C))))
|
||||
|
||||
; w_definition, axiom.
|
||||
(or (= (apply (apply w ?A) ?B) (apply (apply ?A ?B) ?B)))
|
||||
|
||||
; prove_strong_fixed_point, conjecture.
|
||||
(or (/= (apply ?A (f ?A)) (apply (f ?A) (apply ?A (f ?A)))))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,52 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : COL049-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Combinatory Logic
|
||||
; Problem : Strong fixed point for B, W, and M
|
||||
; Version : [WM88] (equality) axioms.
|
||||
; English : The strong fixed point property holds for the set
|
||||
; P consisting of the combinators B, W, and M, where ((Bx)y)z
|
||||
; = x(yz), (Wx)y = (xy)y, Mx = xx.
|
||||
|
||||
; Refs : [Smu85] Smullyan (1978), To Mock a Mocking Bird and Other Logi
|
||||
; : [MW87] McCune & Wos (1987), A Case Study in Automated Theorem
|
||||
; : [WM88] Wos & McCune (1988), Challenge Problems Focusing on Eq
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit
|
||||
; : [Wos93] Wos (1993), The Kernel Strategy and Its Use for the St
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [Ove90]
|
||||
; Names : Problem 2 [WM88]
|
||||
; : CADE-11 Competition Eq-6 [Ove90]
|
||||
; : CL1 [LW92]
|
||||
; : THEOREM EQ-6 [LM93]
|
||||
; : Question 2 [Wos93]
|
||||
; : PROBLEM 6 [Zha93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.22 v2.2.0, 0.14 v2.1.0, 0.62 v2.0.0
|
||||
; Syntax : Number of clauses : 4 ( 0 non-Horn; 4 unit; 1 RR)
|
||||
; Number of literals : 4 ( 4 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 5 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 7 ( 0 singleton)
|
||||
; Maximal term depth : 4 ( 3 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp COL049-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; b_definition, axiom.
|
||||
(or (= (apply (apply (apply b ?A) ?B) ?C) (apply ?A (apply ?B ?C))))
|
||||
|
||||
; w_definition, axiom.
|
||||
(or (= (apply (apply w ?A) ?B) (apply (apply ?A ?B) ?B)))
|
||||
|
||||
; m_definition, axiom.
|
||||
(or (= (apply m ?A) (apply ?A ?A)))
|
||||
|
||||
; prove_strong_fixed_point, conjecture.
|
||||
(or (/= (apply ?A (f ?A)) (apply (f ?A) (apply ?A (f ?A)))))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,78 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : GRP001-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Group Theory
|
||||
; Problem : X^2 = identity => commutativity
|
||||
; Version : [MOW76] axioms.
|
||||
; English : If the square of every element is the identity, the system
|
||||
; is commutative.
|
||||
|
||||
; Refs : [Rob63] Robinson (1963), Theorem Proving on the Computer
|
||||
; : [Wos65] Wos (1965), Unpublished Note
|
||||
; : [MOW76] McCharen et al. (1976), Problems and Experiments for a
|
||||
; : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; Source : [MOW76]
|
||||
; Names : - [Rob63]
|
||||
; : wos10 [WM76]
|
||||
; : G1 [MOW76]
|
||||
; : CADE-11 Competition 1 [Ove90]
|
||||
; : THEOREM 1 [LM93]
|
||||
; : xsquared.ver1.in [ANL]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.00 v2.0.0
|
||||
; Syntax : Number of clauses : 11 ( 0 non-Horn; 8 unit; 5 RR)
|
||||
; Number of literals : 19 ( 1 equality)
|
||||
; Maximal clause size : 4 ( 1 average)
|
||||
; Number of predicates : 2 ( 0 propositional; 2-3 arity)
|
||||
; Number of functors : 6 ( 4 constant; 0-2 arity)
|
||||
; Number of variables : 23 ( 0 singleton)
|
||||
; Maximal term depth : 2 ( 1 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp GRP001-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; left_identity, axiom.
|
||||
(or (product identity ?A ?A))
|
||||
|
||||
; right_identity, axiom.
|
||||
(or (product ?A identity ?A))
|
||||
|
||||
; left_inverse, axiom.
|
||||
(or (product (inverse ?A) ?A identity))
|
||||
|
||||
; right_inverse, axiom.
|
||||
(or (product ?A (inverse ?A) identity))
|
||||
|
||||
; total_function1, axiom.
|
||||
(or (product ?A ?B (multiply ?A ?B)))
|
||||
|
||||
; total_function2, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?A ?B ?D))
|
||||
(= ?C ?D))
|
||||
|
||||
; associativity1, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?B ?D ?E))
|
||||
(not (product ?C ?D ?F))
|
||||
(product ?A ?E ?F))
|
||||
|
||||
; associativity2, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?B ?D ?E))
|
||||
(not (product ?A ?E ?F))
|
||||
(product ?C ?D ?F))
|
||||
|
||||
; square_element, hypothesis.
|
||||
(or (product ?A ?A identity))
|
||||
|
||||
; a_times_b_is_c, hypothesis.
|
||||
(or (product a b c))
|
||||
|
||||
; prove_b_times_a_is_c, conjecture.
|
||||
(or (not (product b a c)))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,98 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : GRP002-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Group Theory
|
||||
; Problem : Commutator equals identity in groups of order 3
|
||||
; Version : [MOW76] axioms.
|
||||
; English : In a group, if (for all x) the cube of x is the identity
|
||||
; (i.e. a group of order 3), then the equation [[x,y],y]=
|
||||
; identity holds, where [x,y] is the product of x, y, the
|
||||
; inverse of x and the inverse of y (i.e. the commutator
|
||||
; of x and y).
|
||||
|
||||
; Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
|
||||
; : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
|
||||
; : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; Source : [MOW76]
|
||||
; Names : G6 [MOW76]
|
||||
; : Theorem 1 [OMW76]
|
||||
; : Test Problem 2 [Wos88]
|
||||
; : Commutator Theorem [Wos88]
|
||||
; : CADE-11 Competition 2 [Ove90]
|
||||
; : THEOREM 2 [LM93]
|
||||
; : commutator.ver1.in [ANL]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.67 v2.2.0, 0.71 v2.1.0, 1.00 v2.0.0
|
||||
; Syntax : Number of clauses : 16 ( 0 non-Horn; 11 unit; 11 RR)
|
||||
; Number of literals : 26 ( 1 equality)
|
||||
; Maximal clause size : 4 ( 1 average)
|
||||
; Number of predicates : 2 ( 0 propositional; 2-3 arity)
|
||||
; Number of functors : 10 ( 8 constant; 0-2 arity)
|
||||
; Number of variables : 26 ( 0 singleton)
|
||||
; Maximal term depth : 2 ( 1 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp GRP002-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; left_identity, axiom.
|
||||
(or (product identity ?A ?A))
|
||||
|
||||
; right_identity, axiom.
|
||||
(or (product ?A identity ?A))
|
||||
|
||||
; left_inverse, axiom.
|
||||
(or (product (inverse ?A) ?A identity))
|
||||
|
||||
; right_inverse, axiom.
|
||||
(or (product ?A (inverse ?A) identity))
|
||||
|
||||
; total_function1, axiom.
|
||||
(or (product ?A ?B (multiply ?A ?B)))
|
||||
|
||||
; total_function2, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?A ?B ?D))
|
||||
(= ?C ?D))
|
||||
|
||||
; associativity1, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?B ?D ?E))
|
||||
(not (product ?C ?D ?F))
|
||||
(product ?A ?E ?F))
|
||||
|
||||
; associativity2, axiom.
|
||||
(or (not (product ?A ?B ?C))
|
||||
(not (product ?B ?D ?E))
|
||||
(not (product ?A ?E ?F))
|
||||
(product ?C ?D ?F))
|
||||
|
||||
; x_cubed_is_identity_1, hypothesis.
|
||||
(or (not (product ?A ?A ?B))
|
||||
(product ?A ?B identity))
|
||||
|
||||
; x_cubed_is_identity_2, hypothesis.
|
||||
(or (not (product ?A ?A ?B))
|
||||
(product ?B ?A identity))
|
||||
|
||||
; a_times_b_is_c, conjecture.
|
||||
(or (product a b c))
|
||||
|
||||
; c_times_inverse_a_is_d, conjecture.
|
||||
(or (product c (inverse a) d))
|
||||
|
||||
; d_times_inverse_b_is_h, conjecture.
|
||||
(or (product d (inverse b) h))
|
||||
|
||||
; h_times_b_is_j, conjecture.
|
||||
(or (product h b j))
|
||||
|
||||
; j_times_inverse_h_is_k, conjecture.
|
||||
(or (product j (inverse h) k))
|
||||
|
||||
; prove_k_times_inverse_b_is_e, conjecture.
|
||||
(or (not (product k (inverse b) identity)))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,53 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : GRP002-3 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Group Theory
|
||||
; Problem : Commutator equals identity in groups of order 3
|
||||
; Version : [Ove90] (equality) axioms : Incomplete.
|
||||
; English : In a group, if (for all x) the cube of x is the identity
|
||||
; (i.e. a group of order 3), then the equation [[x,y],y]=
|
||||
; identity holds, where [x,y] is the product of x, y, the
|
||||
; inverse of x and the inverse of y (i.e. the commutator
|
||||
; of x and y).
|
||||
|
||||
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [Ove90]
|
||||
; Names : CADE-11 Competition Eq-1 [Ove90]
|
||||
; : THEOREM EQ-1 [LM93]
|
||||
; : PROBLEM 1 [Zha93]
|
||||
; : comm.in [OTTER]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.33 v2.2.0, 0.43 v2.1.0, 0.25 v2.0.0
|
||||
; Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 1 RR)
|
||||
; Number of literals : 6 ( 6 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 6 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 8 ( 0 singleton)
|
||||
; Maximal term depth : 5 ( 2 average)
|
||||
|
||||
; Comments : Uses an explicit formulation of the commutator.
|
||||
; : tptp2X -f kif -t rm_equality:rstfp GRP002-3.p
|
||||
;--------------------------------------------------------------------------
|
||||
; left_identity, axiom.
|
||||
(or (= (multiply identity ?A) ?A))
|
||||
|
||||
; left_inverse, axiom.
|
||||
(or (= (multiply (inverse ?A) ?A) identity))
|
||||
|
||||
; associativity, axiom.
|
||||
(or (= (multiply (multiply ?A ?B) ?C) (multiply ?A (multiply ?B ?C))))
|
||||
|
||||
; commutator, axiom.
|
||||
(or (= (commutator ?A ?B) (multiply ?A (multiply ?B (multiply (inverse ?A) (inverse ?B))))))
|
||||
|
||||
; x_cubed_is_identity, hypothesis.
|
||||
(or (= (multiply ?A (multiply ?A ?A)) identity))
|
||||
|
||||
; prove_commutator, conjecture.
|
||||
(or (/= (commutator (commutator a b) b) identity))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,38 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : GRP014-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Group Theory
|
||||
; Problem : Product is associative in this group theory
|
||||
; Version : [Ove90] (equality) axioms : Incomplete.
|
||||
; English : The group theory specified by the axiom given implies the
|
||||
; associativity of multiply.
|
||||
|
||||
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [Ove90]
|
||||
; Names : CADE-11 Competition Eq-4 [Ove90]
|
||||
; : THEOREM EQ-4 [LM93]
|
||||
; : PROBLEM 4 [Zha93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.33 v2.2.0, 0.43 v2.1.0, 0.50 v2.0.0
|
||||
; Syntax : Number of clauses : 2 ( 0 non-Horn; 2 unit; 1 RR)
|
||||
; Number of literals : 2 ( 2 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 5 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 4 ( 0 singleton)
|
||||
; Maximal term depth : 9 ( 4 average)
|
||||
|
||||
; Comments : The group_axiom is in fact a single axiom for group theory
|
||||
; [LM93].
|
||||
; : tptp2X -f kif -t rm_equality:rstfp GRP014-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; group_axiom, axiom.
|
||||
(or (= (multiply ?A (inverse (multiply (multiply (inverse (multiply (inverse ?B) (multiply (inverse ?A) ?C))) ?D) (inverse (multiply ?B ?D))))) ?C))
|
||||
|
||||
; prove_associativity, conjecture.
|
||||
(or (/= (multiply a (multiply b c)) (multiply (multiply a b) c)))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,44 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : LCL024-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Logic Calculi (Equivalential)
|
||||
; Problem : PYO depends on XGK
|
||||
; Version : [Ove90] axioms.
|
||||
; English : Show that Kalman's shortest single axiom for the
|
||||
; equivalential calculus, XGK, can be derived from the Meredith
|
||||
; single axiom PYO.
|
||||
|
||||
; Refs : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr
|
||||
; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; Source : [Ove90]
|
||||
; Names : Test Problem 16 [Wos88]
|
||||
; : XGK and Equivalential Calculus [Wos88]
|
||||
; : CADE-11 Competition 4 [Ove90]
|
||||
; : THEOREM 4 [LM93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.78 v2.2.0, 0.89 v2.1.0, 0.75 v2.0.0
|
||||
; Syntax : Number of clauses : 3 ( 0 non-Horn; 2 unit; 2 RR)
|
||||
; Number of literals : 5 ( 0 equality)
|
||||
; Maximal clause size : 3 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 1-1 arity)
|
||||
; Number of functors : 4 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 5 ( 0 singleton)
|
||||
; Maximal term depth : 5 ( 2 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp LCL024-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; condensed_detachment, axiom.
|
||||
(or (not (is_a_theorem (equivalent ?A ?B)))
|
||||
(not (is_a_theorem ?A))
|
||||
(is_a_theorem ?B))
|
||||
|
||||
; prove_xgk, axiom.
|
||||
(or (is_a_theorem (equivalent ?A (equivalent (equivalent ?B (equivalent ?C ?A)) (equivalent ?C ?B)))))
|
||||
|
||||
; prove_pyo, conjecture.
|
||||
(or (not (is_a_theorem (equivalent (equivalent (equivalent a (equivalent b c)) c) (equivalent b a)))))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,42 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : LCL038-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Logic Calculi (Implication/Falsehood 2 valued sentential)
|
||||
; Problem : C0-1 depends on a single axiom
|
||||
; Version : [McC92] axioms.
|
||||
; English : An axiomatisation for the Implication/Falsehood 2 valued
|
||||
; sentential calculus is {C0-1,C0-2,C0-3,C0-4}
|
||||
; by Tarski-Bernays. Show that C0-1 can be derived from this
|
||||
; suspected single axiom.
|
||||
|
||||
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; Source : [Ove90]
|
||||
; Names : CADE-11 Competition 5 [Ove90]
|
||||
; : THEOREM 5 [LM93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.89 v2.2.0, 1.00 v2.0.0
|
||||
; Syntax : Number of clauses : 3 ( 0 non-Horn; 2 unit; 2 RR)
|
||||
; Number of literals : 5 ( 0 equality)
|
||||
; Maximal clause size : 3 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 1-1 arity)
|
||||
; Number of functors : 4 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 6 ( 2 singleton)
|
||||
; Maximal term depth : 4 ( 2 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp LCL038-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; condensed_detachment, axiom.
|
||||
(or (not (is_a_theorem (implies ?A ?B)))
|
||||
(not (is_a_theorem ?A))
|
||||
(is_a_theorem ?B))
|
||||
|
||||
; single_axiom, axiom.
|
||||
(or (is_a_theorem (implies (implies (implies ?A ?B) ?C) (implies (implies ?C ?A) (implies ?D ?A)))))
|
||||
|
||||
; prove_c0_1, conjecture.
|
||||
(or (not (is_a_theorem (implies (implies a b) (implies (implies b c) (implies a c))))))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,54 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : LCL109-2 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Logic Calculi (Many valued sentential)
|
||||
; Problem : MV-4 depends on the Merideth system
|
||||
; Version : [Ove90] axioms.
|
||||
; Theorem formulation : Wajsberg algebra formulation.
|
||||
; English : An axiomatisation of the many valued sentential calculus
|
||||
; is {MV-1,MV-2,MV-3,MV-5} by Meredith. Wajsberg provided
|
||||
; a different axiomatisation. Show that MV-4 depends on the
|
||||
; Wajsberg system.
|
||||
|
||||
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [LM92] Lusk & McCune (1992), Experiments with ROO, a Parallel
|
||||
; : [LW92] Lusk & Wos (1992), Benchmark Problems in Which Equalit
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; : [Zha93] Zhang (1993), Automated Proofs of Equality Problems in
|
||||
; Source : [Ove90]
|
||||
; Names : CADE-11 Competition Eq-5 [Ove90]
|
||||
; : Luka-5 [LM92]
|
||||
; : MV4 [LW92]
|
||||
; : THEOREM EQ-5 [LM93]
|
||||
; : PROBLEM 5 [Zha93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.56 v2.2.0, 0.71 v2.1.0, 1.00 v2.0.0
|
||||
; Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 1 RR)
|
||||
; Number of literals : 5 ( 5 equality)
|
||||
; Maximal clause size : 1 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 2-2 arity)
|
||||
; Number of functors : 5 ( 3 constant; 0-2 arity)
|
||||
; Number of variables : 8 ( 0 singleton)
|
||||
; Maximal term depth : 4 ( 2 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp LCL109-2.p
|
||||
; ; 'true' renamed to 'true0' - MES
|
||||
;--------------------------------------------------------------------------
|
||||
; wajsberg_1, axiom.
|
||||
(or (= (implies true0 ?A) ?A))
|
||||
|
||||
; wajsberg_2, axiom.
|
||||
(or (= (implies (implies ?A ?B) (implies (implies ?B ?C) (implies ?A ?C))) true0))
|
||||
|
||||
; wajsberg_3, axiom.
|
||||
(or (= (implies (implies ?A ?B) ?B) (implies (implies ?B ?A) ?A)))
|
||||
|
||||
; wajsberg_4, axiom.
|
||||
(or (= (implies (implies (not ?A) (not ?B)) (implies ?B ?A)) true0))
|
||||
|
||||
; prove_wajsberg_mv_4, conjecture.
|
||||
(or (/= (implies (implies (implies a b) (implies b a)) (implies b a)) true0))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,55 +0,0 @@
|
|||
%------------------------------------------------------------------------------
|
||||
% File : LCL111-1 : TPTP v3.0.0. Released v1.0.0.
|
||||
% Domain : Logic Calculi (Many valued sentential)
|
||||
% Problem : MV-25 depends on the Merideth system
|
||||
% Version : [McC92] axioms.
|
||||
% English : An axiomatisation of the many valued sentential calculus
|
||||
% is {MV-1,MV-2,MV-3,MV-5} by Meredith. Show that MV-25 depends
|
||||
% on the Meredith system.
|
||||
|
||||
% Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
% : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
|
||||
% : [McC92] McCune (1992), Email to G. Sutcliffe
|
||||
% : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
% : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
% Source : [McC92]
|
||||
% Names : CADE-11 Competition 6 [Ove90]
|
||||
% : MV-57 [MW92]
|
||||
% : THEOREM 6 [LM93]
|
||||
% : mv.in part 2 [OTTER]
|
||||
% : mv25.in [OTTER]
|
||||
% : ovb6 [SETHEO]
|
||||
|
||||
% Status : Unsatisfiable
|
||||
% Rating : 0.00 v2.4.0, 0.43 v2.3.0, 0.14 v2.2.1, 0.11 v2.2.0, 0.22 v2.1.0, 0.25 v2.0.0
|
||||
% Syntax : Number of clauses : 6 ( 0 non-Horn; 5 unit; 2 RR)
|
||||
% Number of atoms : 8 ( 0 equality)
|
||||
% Maximal clause size : 3 ( 1 average)
|
||||
% Number of predicates : 1 ( 0 propositional; 1-1 arity)
|
||||
% Number of functors : 5 ( 3 constant; 0-2 arity)
|
||||
% Number of variables : 11 ( 1 singleton)
|
||||
% Maximal term depth : 4 ( 3 average)
|
||||
|
||||
% Comments :
|
||||
% : tptp2X -f tptp:short LCL111-1.p
|
||||
%------------------------------------------------------------------------------
|
||||
cnf(condensed_detachment,axiom,(
|
||||
~ is_a_theorem(implies(X,Y))
|
||||
| ~ is_a_theorem(X)
|
||||
| is_a_theorem(Y) )).
|
||||
|
||||
cnf(mv_1,axiom,(
|
||||
is_a_theorem(implies(X,implies(Y,X))) )).
|
||||
|
||||
cnf(mv_2,axiom,(
|
||||
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )).
|
||||
|
||||
cnf(mv_3,axiom,(
|
||||
is_a_theorem(implies(implies(implies(X,Y),Y),implies(implies(Y,X),X))) )).
|
||||
|
||||
cnf(mv_5,axiom,(
|
||||
is_a_theorem(implies(implies(not(X),not(Y)),implies(Y,X))) )).
|
||||
|
||||
cnf(prove_mv_25,negated_conjecture,(
|
||||
~ is_a_theorem(implies(implies(a,b),implies(implies(c,a),implies(c,b)))) )).
|
||||
%------------------------------------------------------------------------------
|
|
@ -1,53 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : LCL114-1 : TPTP v2.2.0. Released v1.0.0.
|
||||
; Domain : Logic Calculi (Many valued sentential)
|
||||
; Problem : MV-36 depnds on the Merideth system
|
||||
; Version : [McC92] axioms.
|
||||
; English : An axiomatisation of the many valued sentential calculus
|
||||
; is {MV-1,MV-2,MV-3,MV-5} by Meredith. Show that 36 depends
|
||||
; on the Meredith system.
|
||||
|
||||
; Refs : [Ove90] Overbeek (1990), ATP competition announced at CADE-10
|
||||
; : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
|
||||
; : [McC92] McCune (1992), Email to G. Sutcliffe
|
||||
; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal
|
||||
; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11
|
||||
; Source : [McC92]
|
||||
; Names : CADE-11 Competition 7 [Ove90]
|
||||
; : MV-60 [MW92]
|
||||
; : THEOREM 7 [LM93]
|
||||
|
||||
; Status : unsatisfiable
|
||||
; Rating : 0.89 v2.1.0, 0.88 v2.0.0
|
||||
; Syntax : Number of clauses : 6 ( 0 non-Horn; 5 unit; 2 RR)
|
||||
; Number of literals : 8 ( 0 equality)
|
||||
; Maximal clause size : 3 ( 1 average)
|
||||
; Number of predicates : 1 ( 0 propositional; 1-1 arity)
|
||||
; Number of functors : 4 ( 2 constant; 0-2 arity)
|
||||
; Number of variables : 11 ( 1 singleton)
|
||||
; Maximal term depth : 4 ( 2 average)
|
||||
|
||||
; Comments :
|
||||
; : tptp2X -f kif -t rm_equality:rstfp LCL114-1.p
|
||||
;--------------------------------------------------------------------------
|
||||
; condensed_detachment, axiom.
|
||||
(or (not (is_a_theorem (implies ?A ?B)))
|
||||
(not (is_a_theorem ?A))
|
||||
(is_a_theorem ?B))
|
||||
|
||||
; mv_1, axiom.
|
||||
(or (is_a_theorem (implies ?A (implies ?B ?A))))
|
||||
|
||||
; mv_2, axiom.
|
||||
(or (is_a_theorem (implies (implies ?A ?B) (implies (implies ?B ?C) (implies ?A ?C)))))
|
||||
|
||||
; mv_3, axiom.
|
||||
(or (is_a_theorem (implies (implies (implies ?A ?B) ?B) (implies (implies ?B ?A) ?A))))
|
||||
|
||||
; mv_5, axiom.
|
||||
(or (is_a_theorem (implies (implies (not ?A) (not ?B)) (implies ?B ?A))))
|
||||
|
||||
; prove_mv_36, conjecture.
|
||||
(or (not (is_a_theorem (implies (implies a b) (implies (not b) (not a))))))
|
||||
|
||||
;--------------------------------------------------------------------------
|
|
@ -1,155 +0,0 @@
|
|||
;--------------------------------------------------------------------------
|
||||
; File : PUZ031+1 : TPTP v2.2.0. Released v2.0.0.
|
||||
; Domain : Puzzles
|
||||
; Problem : Schubert' |