Difference between revisions of "TPDB"
From Termination-Portal.org
Jump to navigationJump to search (fixed links to more recent versions of converter) |
(→Syntax and semantics specification: Link to new TPDB) |
||
| (14 intermediate revisions by 3 users not shown) | |||
| Line 4: | Line 4: | ||
== Syntax and semantics specification == | == Syntax and semantics specification == | ||
| − | + | * for versions from 11.* onwards (XML format): [https://github.com/TermCOMP/TPDB/raw/master/xml/xtc.xsd xtc.xsd], already part of the [https://github.com/TermCOMP/TPDB TPDB] | |
| − | * for versions from 7.* onwards (XML format): http:// | + | * for versions from 7.* onwards (XML format): [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc.xsd xtc.xsd], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB] |
* for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html | * for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html | ||
| Line 13: | Line 13: | ||
== Data == | == Data == | ||
| + | * version 11.0 (2019): https://github.com/TermCOMP/TPDB | ||
| + | * version 9.0 (2014), 10.3 (2015), 10.4 (2016), 10.5 (2017), 10.6 (2018) http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB | ||
* version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2012) and 8.0.7 (2013) http://termcomp.uibk.ac.at/status/downloads/ | * version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2012) and 8.0.7 (2013) http://termcomp.uibk.ac.at/status/downloads/ | ||
* version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz | * version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz | ||
| Line 19: | Line 21: | ||
== Sources == | == Sources == | ||
| + | |||
| + | TPDB problems are collected from a variety of sources, by a variety of contributors. Often, the author of the problem is not the creator of the respective TPDB file. Sometimes, TPDB file structure (directory names) have been changed. | ||
The following are references for classical problem sets that appear in TPDB. | The following are references for classical problem sets that appear in TPDB. | ||
| Line 25: | Line 29: | ||
* TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf | * TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf | ||
* TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps | * TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps | ||
| − | * SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?) | + | * SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?). They include (as z027 .. z064) a set of one-rule termination problems by Alfons Geser (Habilitationsschrift, Tübingen, 2001) and possibly Winfried Kurth (Dissertation, Clausthal, 1990) |
| + | |||
| + | And here are some extra bits of trivia. | ||
| − | + | * SRS termination problems ICFP_2010 and ICFP_2010_relative were produced by participants of the ICFP 2010 programming contest, organized by Bertram Felgenhauer and Johannes Waldmann. ''All'' of these problems are terminating by construction. See https://www.imn.htwk-leipzig.de/~waldmann/talk/10/icfp/ | |
== Tools == | == Tools == | ||
| − | * converter from pre-7 (textual) format to 7.* (XML) format: http:// | + | * converter from pre-7 (textual) format to 7.* (XML) format: http://cl-informatik.uibk.ac.at/users/thiemann/convert.jar, usage: |
java -jar convert.jar someTrs.trs > someTrs.xml | java -jar convert.jar someTrs.trs > someTrs.xml | ||
| − | * converter from 7.* (XML) format to pre-7 (textual) format: http:// | + | * converter from 7.* (XML) format to pre-7 (textual) format: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtc2tpdb.xsl xtc2tpdb.xsl], already part of the [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB TPDB], usage: |
xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs | xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs | ||
| + | |||
| + | * converter from 7.* (XML) format to HTML: [http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/raw-file/tip/xml/xtcHTML.xsl xtcHTML.xsl], see explanation at http://lists.lri.fr/pipermail/termtools/2018-July/001212.html | ||
* Haskell library for reading and writing TPDB (plain and XML format) [http://hackage.haskell.org/package/tpdb] | * Haskell library for reading and writing TPDB (plain and XML format) [http://hackage.haskell.org/package/tpdb] | ||
Latest revision as of 02:08, 18 June 2020
The Termination Problems Data Base collects termination problems that are being used in termination competitions.
Syntax and semantics specification
- for versions from 11.* onwards (XML format): xtc.xsd, already part of the TPDB
- for versions from 7.* onwards (XML format): xtc.xsd, already part of the TPDB
- for versions up to 5.*: http://www.lri.fr/~marche/tpdb/format.html
see also:
- output specification for certified categories: http://cl-informatik.uibk.ac.at/software/cpf/
Data
- version 11.0 (2019): https://github.com/TermCOMP/TPDB
- version 9.0 (2014), 10.3 (2015), 10.4 (2016), 10.5 (2017), 10.6 (2018) http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB
- version 7.* (2009), 8.0 (2010), 8.0.1 (2011), 8.0.6 (2012) and 8.0.7 (2013) http://termcomp.uibk.ac.at/status/downloads/
- version 6.0.2 http://termcomp.uibk.ac.at/termcomp/docs/tpdb-6.0.2.tar.gz
- version 5.0.2 (2008..2009) http://termcomp.uibk.ac.at/termcomp/docs/tpdb-5.0.2.tar.gz
- earlier versions (2003 .. 2007) http://www.lri.fr/~marche/tpdb/
Sources
TPDB problems are collected from a variety of sources, by a variety of contributors. Often, the author of the problem is not the creator of the respective TPDB file. Sometimes, TPDB file structure (directory names) have been changed.
The following are references for classical problem sets that appear in TPDB.
- TRS/SK90 Joachim Steinbach, Ulrich Kühler: Check your Ordering - termination proofs and open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990.
- TRS/D33 Nachum Dershowitz: 33 Examples of Termination, 1995 Proc. French Spring School of Theoretical Computer Science, LNCS 909, http://www.math.tau.ac.il/~nachumd/papers/printemp-print.pdf
- TRS/AG01 Thomas Arts, Jürgen Giesl: Termination of term rewriting using dependency pairs, 2000, http://dblp.uni-trier.de/rec/bibtex/journals/tcs/ArtsG00 http://verify.rwth-aachen.de/giesl/papers/ibn-97-46.ps
- SRS/Zantema 128 string rewriting termination problems collected by Hans Zantema (2004?). They include (as z027 .. z064) a set of one-rule termination problems by Alfons Geser (Habilitationsschrift, Tübingen, 2001) and possibly Winfried Kurth (Dissertation, Clausthal, 1990)
And here are some extra bits of trivia.
- SRS termination problems ICFP_2010 and ICFP_2010_relative were produced by participants of the ICFP 2010 programming contest, organized by Bertram Felgenhauer and Johannes Waldmann. All of these problems are terminating by construction. See https://www.imn.htwk-leipzig.de/~waldmann/talk/10/icfp/
Tools
- converter from pre-7 (textual) format to 7.* (XML) format: http://cl-informatik.uibk.ac.at/users/thiemann/convert.jar, usage:
java -jar convert.jar someTrs.trs > someTrs.xml
- converter from 7.* (XML) format to pre-7 (textual) format: xtc2tpdb.xsl, already part of the TPDB, usage:
xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs
- converter from 7.* (XML) format to HTML: xtcHTML.xsl, see explanation at http://lists.lri.fr/pipermail/termtools/2018-July/001212.html
- Haskell library for reading and writing TPDB (plain and XML format) [1]
