Hello, I'm interested in utilizing the benchmark in TPDB for conducting experiments on verification tools. However, I'm uncertain about the ground truth for these cases, specifically, whether a case is terminating or non-terminating. Could you kindly provide guidance on how to determine the termination status of these cases? Thank you!
Hi, TPDB is a database where the ground truth is not always known. There are problems in TPDB whose termination behavior corresponds to famous mathematical problems, e.g., Collatz conjecture, the Goldbach conjecture, etc. The best you can do is to look at the results of the termination competition: for those problems where there is a certified answer (indicated by a checkmark), you can take that answer as ground-truth. For instance, this link shows you results for plain first-order TRSs: https://termcomp.github.io/Y2023/TRS_Standard.html Best, René
Am 09.10.2023 um 16:28 schrieb Zhang Yao <zzyy@tju.edu.cn>:
Hello,
I'm interested in utilizing the benchmark in TPDB for conducting experiments on verification tools. However, I'm uncertain about the ground truth for these cases, specifically, whether a case is terminating or non-terminating. Could you kindly provide guidance on how to determine the termination status of these cases?
Thank you!
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
participants (2)
-
Thiemann, René -
Zhang Yao