Papers on WinKE and KE

Papers related to the WinKE Software:

• U. Endriss. The Interactive Learning Environment WinKE for Teaching Deductive Reasoning In M. Manzano, editor, First International Congress on Tools for Teaching Logic, Proceedings, University of Salamanca, Spain, 2000. Invited talk. (4 pages)
• U. Endriss. Using Interaction and Visualisation for Teaching Deductive Reasoning. In G. Cumming, T. Okamoto, and L. Gomez, editors, Advanced Research in Computers and Communications in Education, Proceedings of ICCE'99, Tokyo, Frontiers in Artificial Intelligence and Applications Series, Vol. 55-2, IOS Press, 1999. Recipient of the Jan Hawkins Award. (4 pages)
• U. Endriss. An Interactive Theorem Proving Assistant. In N. Murray, editor, Analytic Tableaux and Related Methods. Proceedings of TABLEAUX'99, Saratoga Springs (NY), LNAI 1617, Springer-Verlag, 1999. (5 pages)
• M. D'Agostino, U. Endriss, D. Gabbay, M. Mondadori, and J. Pitt. WinKE: A Pedagogic Tool for Teaching Logic and Reasoning. Abstract published in B. Goettl, H. Halff, C. Redfield, V. Shute, editors, Intelligent Tutoring Systems, 4th International Conference, ITS'98, San Antonio, Texas, Proceedings, LNCS 1452, Springer-Verlag, 1998. Have a look at the poster.
• M. D'Agostino and U. Endriss. WinKE: A Proof Assistant for Teaching Logic. Proceedings of the First International Workshop on Labelled Deduction, Freiburg, 1998. (7 pages)
• U. Endriss. An Overview of the WinKE System, 1998. (25 pages)
• M. D'Agostino, U. Endriss, D. Gabbay, M. Mondadori, and J. Pitt. Un Nuovo Approccio alla Meccanizzazione del Ragionamento Deduttivo. Conference of the Italian Philosophical Society on "Man and Machine: thirty years later", University of Bari, 1997.
• U. Endriss. A KE Based Theorem Proving Assistant. Master's Thesis, Imperial College, London, 1996. (61 pages)
• J. Pitt. MacKE: Yet Another Proof Assistant & Automated Pedagogic Tool. in P. Baumgärtner, R. Hähnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, Springer-Verlag, 1995.

Papers related to the KE Calculus:

• M. D'Agostino, D. Gabbay, and A. Russo. Grafting Modalities onto Substructural Implication Systems. In Studia Logica, 59, 1997. (40 pages)
• M. D'Agostino and D. Gabbay. A Generalization of Analytic Deduction via Labelled Deductive Systems. Part I: Basic Substructural Logics, Journal of Automated Reasoning, 13, 1994. (46 pages)
• K. Broda, M. D'Agostino, and M. Mondadori. A Solution to a Problem of Popper. In Karl Popper, Philosopher of Science, Proceedings of the conference The Epistemology of Karl Popper, Cesena, October 1994, Kluwer Academic Publishers, to appear. (22 pages)
• M. D'Agostino and M. Mondadori. The Taming of the Cut. Classical Refutations with Analytic Cut. Journal of Logic and Computation, 4, 1994. (38 pages)
• M. D'Agostino. Are Tableaux an Improvement on Truth Tables? Cut-free Proofs and Bivalence. Journal of Logic, Language and Information, 1, 1992. (20 pages)
• M. D'Agostino. Investigations into the Complexity of some Propositional Calculi. Oxford University Computing Laboratory, Technical Monograph PRG-88, ISBN 0-902928-67-8, 1990. (129 pages)

Papers related to Proof Procedures for KE:

• U. Endriss. A Time Efficient KE Based Theorem Prover. In N. Murray, editor, Analytic Tableaux and Related Methods, Proceedings of TABLEAUX'99, Saratoga Springs (NY), LNAI 1617, Springer-Verlag, 1999. (6 pages)
• J. Pitt and J. Cunningham. Distributed Modal Theorem Proving with KE. In P. Miglioli, U. Moscato, D. Mundici, M. Oraghi, editors, Analytic Tableaux and Related Methods, Proceedings of TABLEAUX'96, LNAI 1071, 1996.
• J. Pitt and J. Cunningham. Theorem Proving and Model Building with the Calculus KE. Bulletin of the IGPL, 4, 1995.