Benchmark Evaluation of □KE

  • Jeremy Pitt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


Prover: We used □KE (no version number), which was designed to be a generic theorem prover for the family of 15 normal model logics.


  1. 1.
    M. D’Agostino and M. Mondadori. The Taming of the Cut. Journal of Logic and Computation, 4:285–319, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    M. Fitting. Basic modal logic. In D. Gabbay, C. Hogger, & J. Robinson, eds., Handbook of Logic in AI and Logic Programming, vol.1, pp368–448. OUP, 1993.Google Scholar
  3. 3.
    J. Pitt and J. Cunningham. Distributed modal theorem proving with KE. In P. Miglioli, U. Moscato, D. Mundici, & M. Ornaghi, eds., Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, pp160–176. Springer-Verlag, 1996.Google Scholar
  4. 4.
    J. Pitt and J. Cunningham. Theorem proving and model building with the calculus KE. Journal of the IGPL, 4(1):129–150, 1996.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Jeremy Pitt
    • 1
  1. 1.Department of Electrical & Electronic EngineeringImperial College of Science Technology & MedicineEngland

Personalised recommendations