Abstract
Previous methods for generating random modal formulae (for the multi-modal logic K (m) ) result either in flawed test sets or formulae that are too hard for current modal decision procedures and, also, unnatural. We present here a new system and generation methodology which results in unflawed test sets and more-natural formulae that are better suited for current decision procedures.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and A. Tacchella. SAT vs. Translation based decision procedures for modal logics: a comparative evaluation. Journal of Applied Non-Classical Logics, 10(2):145–172, 2000.
E. Giunchiglia, F. Giunchiglia, and A. Tacchella. SAT Based Decision Procedures for Classical Modal Logics. To appear in Journal of Automated Reasoning., 2001.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. CADE13, number 1104 in Lecture Notes in Artificial Intelligence, pages 583–597, Berlin, August 1996. Springer-Verlag.
I. Horrocks. Using an expressive description logic: FaCT or fiction? In Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR‘98), pages 636–647, 1998.
Ian Horrocks, Peter F. Patel-Schneider, and Roberto Sebastiani. An analysis of empirical testing for modal decision procedures. Logic Journal of the IGPL, 8(3):293–323, 2000.
Ullrich Hustadt and Renate A. Schmidt. An empirical analysis of modal theorem provers. Journal of Applied Non-Classical Logics, 9(4):479–522, 1999.
F. Massacci. Design and Results of Tableaux-99 Non-Classical (Modal) System Competition. In Automated Reasoning with Analytic Tableaux and Related Methods: International Conference (Tableaux‘99), number 1617 in Lecture Notes in Artificial Intelligence, pages 14–18, Berlin, 1999. Springer-Verlag.
Peter F. Patel-Schneider. DLP system description. In E. Franconi, G. De Giacomo, R. M. MacGregor, W. Nutt, C. A. Welty, and F. Sebastiani, editors, Collected Papers from the International Description Logics Workshop (DL‘98), pages 87–89, 1998. Available as CEUR-WS/Vol-11 from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Patel-Schneider, P.F., Sebastiani, R. (2001). A New System and Methodology for Generating Random Modal Formulae. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_40
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive