The aim of the TABLEAUX-2000 Non-Classical (Modal) System Comparisons (TANCS-2000) is to provide a set of benchmarks and a standardized methodology for the assessment and comparison of ATP systems in non-classical logics, as it is done for first-order logic with the CADE System Competition. We believe that TANCS can benefit the scientific community in two ways: by promoting the competition among ATP systems and thus yielding novel solutions, and by providing a scientific design for benchmarking non-classical ATP systems. This paper reports the main ideas behind the design, the benchmarks, the organization, and the rating of the ATP systems of TANCS-2000. © Springer-Verlag Berlin Heidelberg 2000.
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000|
|Period||3/07/00 → 7/07/00|