TANCS is a Non Classical System Comparison. It was organised in 1998 and 2000 in conjunction with the TABLEAUX Conferences.
Problems used at the TANCS-2000 modal logic theorem prover competition are stored at this site, archived and compressed with bzip2.
The problems are available in different formats:
The problems are (translations of) benchmarks used in tests performed with MSPASS in the TANCS'2000 competition of non-classical (modal and description) logic systems [HS00a,MD00]. The original problems belong to modal logic K and tense logic Kt, which are decidable logics, they have the f.m.p. and are PSPACE-complete. The translation of the problems to first-order logic was done with MSPASS using
The translated problems are all decidable by resolution -- the class in 1. by unrefined resolution and condensing [S99], and the classes in 2. and 3. by ordered resolution [HS00b]. Class 1. problems belong to the Bernays-Schoenfinkel class and have special syntactic properties, which can be exploited by theorem provers based on propositional SAT.
Problems in the files p-psat-* belong to class 2.
Problems in the files p-qbf-cpdl-* belong to class 3.
All others belong to class 1.
[HS00a] Hustadt, U. and Schmidt, R. A. (2000), "MSPASS: Modal Reasoning by Translation and First-Order Resolution". In Dyckhoff, R. (eds), "Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX'2000)". Lecture Notes in Artificial Intelligence, Vol. 1847, Springer, 67-71.
[HS00b] Hustadt, U. and Schmidt, R. A. (2000), "Issues of Decidability for Description Logics in the Framework of Resolution". In Caferra, R. and Salzer, G. (eds), "Automated Deduction in Classical and Non-Classical Logics". Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, 191-205.
[MD00] Massacci, F. and Donini, F. M. (2000), "Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison". In Dyckhoff, R. (eds), "Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX'2000)". Lecture Notes in Artificial Intelligence, Vol. 1847, Springer, 52-56.
[S99] Schmidt, R. A. (1999), "Decidability by Resolution for Propositional Modal Logics". Journal of Automated Reasoning, Vol. 22, 4, 379-396.