Abstract
This paper reports the main ideas behind the design, the benchmarks, the organization, and the rating of the ATP systems of the TABLEAUX-99 Non-Classical (Modal) System Comparisons (TANCS).
More details are at htpp://www.dis.uniromal.it/~massacci/TANCS.
I would like to thank F. Donini, R. Goré, P. Liberatore, N. Murray, and A. Voronkov. This work has been supported by a CNR fellowship and by CNR and MURST grants.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Balsinger & A. Heuerding. Comparison of theorem provers for modal logics. In Proc. of TABLEAUX-98, LNAI 1397, p. 25–27, Springer Verlag 1998.
M. Cadoli, A. Giovanardi, & M. Schaerf. An algorithm to evaluate quantified boolean formulae. In Proc. of AAAI-98, 1998.
F. Donini, M. Lenzerini, D. Nardi, & A. Schaerf. Reasoning in description logics. In Foundation of Knowledge Representation, p. 191–236. CSLI-Publications, 1996.
M. Fitting. Basic modal logic. In Handbook of Logic in AI and Logic Programming, vol. 1, p. 365–448. Oxford Univ. Press, 1993.
P. Fleming & J. Wallace. How not to lie with statistics: the correct way to sum marize benchmark results. CACM, 29(3):218–221, 1986.
E. Giunchiglia, F. Giunchiglia, R. Sebastiani, & A. Tacchella. More evaluation of decision procedures for modal logics. In Proc. of KR-96, p. 626–635. 1998.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal k. In Proc. of CADE-96, LNAI 1104, p. 583–597. Springer-Verlag, 1996.
J. Halpern. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. AH, 75(2):361–372, 1995.
J. Y. Halpern & Y. Moses. A guide to completeness and complexity for modal logics of knowledge and belief. AIJ, 54:319–379, 1992.
U. Hustadt & R. Schmidt. On evaluating decision procedure for modal logic. In Proc. of IJCAI-97, p. 202–207, 1997.
D. Johnson. A theoretician’s guide to the experimental analysis of algorithms. Invited talk at AAAI-96. See http://www.research.att.com/~dsj, Aug. 1996.
D. Johnson & M. Trick, editors. Cliques, Coloring, Satisfiability: the second DIMACS implementation challenge, vol. 26 of AMS Series in Discr. Math. and Theor. Comp. Sci.. Am. Math. Soc., 1996.
D. Johnson. A catalog of complexity classes. In Handbook of Theoretical Computer Science, p. 67–162. Elsevier Science, 1990.
R. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM JoC, 6(3):467–480, 1977.
J. Orlin. The complexity of dynamic languages and dynamic optimization prob lems. In Proc. of STOC-81, p. 218–227, 1981.
W. Press, B. Flannery, S. Teukolsky, & W. Vetterling. Numerical Recipes in C: The Art of Scientific Computing. Cambridge Univ. Press, 1990.
B. Selman, D. Mitchell, & H. Levesque. Generating hard satisfiability problems. AIJ, 81(1–2):17–29, 1996.
C. Suttner & G. Sutcliffe. The CADE-14 ATP system competition. JAR, 21(1):99–134, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Massacci, F. (1999). Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_2
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive