Teaching Smullyan's Analytic Tableaux in a Scalable Learning Environment

Reference:

Tomi Janhunen, Toni Jussila, Matti Järvisalo, and Emilia Oikarinen. Teaching Smullyan's analytic tableaux in a scalable learning environment. In Ari Korhonen and Lauri Malmi, editors, Kolin Kolistelut – Koli Calling. Proceedings of the Fourth Finnish / Baltic Sea Conference on Computer Science Education, volume TKO-42/04 of Research Report Series of Laboratory of Information Processing Science, Helsinki University of Technology, pages 85–94. Otamedia, December 2004.

Abstract:

This paper describes an automated learning environment in which various kinds of formal systems such as logic, automata and grammars can be taught on basic courses in (theoretical) computer science. A central design criteria of the system is scalability as hundreds of students are expected to participate in courses which are using the system to automate their home assignment processes. High numbers of students imply the need for automated, partially randomized assignment generators in order to create challenging problem instances for students as well as to minimize plagiarism. In this paper, we consider the case of Smullyan's tableau method as a concrete example and discuss in further detail the design of a generator for logical problems which are to be solved by the student. The non-deterministic nature of tableau proofs is identified as a factor that makes the automated generation of assignments much harder than generating assignments which are solvable just by following some deterministic algorithm. Moreover, the minimum number of branching nodes in the respective tableau proof is proposed as a criterion for measuring the quality of a problem instance. The same criterion is then used to re-evaluate tableau proofs that were submitted by our students in years 2000–2004.

Suggested BibTeX entry:

@inproceedings{JJJO04:kolicall,
    author = {Tomi Janhunen and Toni Jussila and Matti J\"arvisalo and Emilia Oikarinen},
    booktitle = {Kolin Kolistelut -- Koli Calling. Proceedings of the Fourth Finnish / Baltic Sea Conference on Computer Science Education},
    editor = {Ari Korhonen and Lauri Malmi},
    month = {December},
    pages = {85--94},
    publisher = {Otamedia},
    series = {Research Report Series of Laboratory of Information Processing Science, Helsinki University of Technology},
    title = {Teaching {S}mullyan's Analytic Tableaux in a Scalable Learning Environment},
    volume = {TKO-42/04},
    year = {2004},
}