Benchmark Problems for Modal and Description Logics

TANCS 2000 Problems

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

  1. the optimised functional translation in terms of n-ary predicates for the modal QBF formulae (flag settings -EMLTranslation=2 -EMLFuncNary=1),
  2. the relational translation for the PSAT problems (flag settings -EMLTranslation=0 -EMLFuncNary=0), and
  3. the relational translation with renaming on *-free converse PDL formulae (flag settings -EMLTranslation=0 -EMLFuncNary=0 -CNFRenOps=1).

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.

References:

[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.


MSPASS
Web Interactive Input Form | Web Upload Form | Documentation

Last modified: 27 Nov 15
Copyright © 1999-2015 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk