Package: tptp
Description: Thousands of Problems for Theorem Provers
Homepage: http://www.tptp.org
Version: 6.1.0
Revision: 2
License: OSI-Approved
Source: http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v%v.tgz
Source-Checksum: SHA256(64cf33d159869475901a8b9460d52419b3cd1926eb76aa7b4cc1409cfa049714)
PatchFile: %n.patch
PatchFile-MD5: 4e89c91c321e5ff651f4a3687afeaec9
PatchScript: sed 's|@PREFIX@|%p|g' < %{PatchFile} | patch -p1
DescDetail: <<
The TPTP (Thousands of Problems for Theorem Provers) Problem Library
is a library of test problems for automated theorem proving (ATP)
systems. The TPTP supplies the ATP community with:

* A comprehensive library of the ATP test problems that are available
today, in order to provide an overview and a simple, unambiguous
reference mechanism.

* A comprehensive list of references and other interesting information
for each problem.

* New generalized variants of problems whose original presentation is
hand-tailored towards a particular automated proof.

* Arbitrary size instances of generic problems (e.g., the N-queens
problem).

* A utility to convert the problems to existing ATP formats. Currently
the Bliksem, CARINE, Dedam, DFG, DIMACS, FINDER, KIF, Otter, PROTEIN,
Prover9, PTTP, Satchmo, SCOTT, SEM, SETHEO, THINKER, Waldmeister
formats are supported, and other formats can be easily produced.

* General guidelines outlining the requirements for ATP system
evaluation.

The principal motivation for the TPTP is to support the testing and
evaluation of ATP systems, to help ensure that performance results
accurately reflect the capabilities of the ATP system being
considered. A common library of problems is necessary for meaningful
system evaluations, meaningful system comparisons, repeatability of
testing, and the production of statistically significant results. The
TPTP is such a library.
<<
Maintainer: Jesse Alama <jesse.alama@gmail.com>
CompileScript: <<
<<
InstallScript: <<

  # TPTP2X
  mkdir -p %i/share/tptp/TPTP2X
  find TPTP2X -type f -name 'format.*'    -exec install -m 644 {} %i/share/tptp/TPTP2X ';'
  find TPTP2X -type f -name 'tptp2X.*'    -exec install -m 644 {} %i/share/tptp/TPTP2X ';'
  find TPTP2X -type f -name 'transform.*' -exec install -m 644 {} %i/share/tptp/TPTP2X ';'
  find TPTP2X -type f -name 'tptp2X.*' -exec install -m 644 {} %i/share/tptp/TPTP2X ';'

  mkdir -p %i/bin
  install -m 755 TPTP2X/tptp2X %i/bin

  # scripts and generators
  mkdir -p %i/bin
  install -m 755 Scripts/tptp2T %i/bin
  mkdir -p %i/lib/tptp
  find Generators -type f -exec install -m 644 {} %i/lib/tptp ';'

  # axioms and problems
  mkdir -p %i/share/tptp
  cp -R Axioms %i/share/tptp
  cp -R Problems %i/share/tptp

  # documentation
  mkdir -p %i/share/doc/tptp
  cp -R Documents/* %i/share/doc/tptp

<<
RuntimeVars: <<
  TPTP: %p/share/tptp
<<
Depends: tptp2x, tptp-axioms, tptp-problems
Recommends: tptp2x
SplitOff: <<
  Package: tptp2x
  Description: Transform TPTP files into other formats
  Recommends: tptp
  Depends: swi-prolog, gawk
  Files: <<
    bin/tptp2x
    share/tptp/TPTP2X/*
<<
  DocFiles: TPTP2X/ReadMe
<<
SplitOff2: <<
  Package: tptp-generators
  Description: Generate theorem proving problems
  Recommends: swi-prolog
  Files: <<
    lib/tptp/*.g
<<
<<
SplitOff3: <<
  Package: tptp-axioms
  Description: Axioms for the TPTP Problem Library
  Files: share/tptp/Axioms
  Suggests: tptp-problems
<<
SplitOff4: <<
  Package: tptp-problems
  Description: The TPTP Problem Library
  Depends: tptp-axioms
  Files: share/tptp/Problems
<<