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.

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

AUTHORS:

ABSTRACT: