A New Method for Testing Decision Procedures in Modal and Terminological Logics

We present a new methodology for testing decision procedures for modal and terminological logics which extends the fixed-clause-length test model, commonly used for propositional satisfiability testing. The new method is easy to implement and to use, and it allows for a statistical control of some important features, e.g., hardness and satisfiability rate, of the formulas generate