Search

Search Results

• Sage and scribe – asymmetrical pair work that can easily fit into any mathematics lesson, yet still have cooperative benefits

  133-164

  Eszter Kovács-Kószó

  Viktória Czakó

  József Kosztolányi

  Views:

  850

  This article uses a case study experiment to learn the characteristics of a pair work, called the sage and scribe method (Kagan, 2008). We also wished to explore the positive and negative effects of the systematic application of this single cooperative element without any other structural changes during the lessons. In the case study experiment, we asked two teachers, accustomed to traditional frontal teaching methods, to substitute individual work tasks in their standard lesson plans with the sage and scribe method. Our experiments indicate that this method wastes insignificant time, requires little extra effort on the part of the teacher, yet has many of the positive effects of cooperative methods: in our experiments, students received immediate feedback, corrected each other’s mistakes, learned from each other in meaningful discussions and engaged in collaborative reasoning to address emerging problems.

  Subject Classification: 97D40

• Linear clause generation by Tableaux and DAGs

  109-118

  Gergely Kovásznai

  Views:

  202

  Clause generation is a preliminary step in theorem proving since most of the state-of-the-art theorem proving methods act on clause sets. Several clause generating algorithms are known. Most of them rewrite a formula according to well-known logical equivalences, thus they are quite complicated and produce not very understandable information on their functioning for humans. There are other methods that can be considered as ones based on tableaux, but only in propositional logic. In this paper, we propose a new method for clause generation in first-order logic. Since it inherits rules from analytic tableaux, analytic dual tableaux, and free-variable tableaux, this method is called clause generating tableaux (CGT). All of the known clause generating algorithms are exponential, so is CGT. However, by switching to directed acyclic graphs (DAGs) from trees, we propose a linear CGT method. Another advantageous feature is the detection of valid clauses only by the closing of CGT branches. Last but not least, CGT generates a graph as output, which is visual and easy-to-understand. Thus, CGT can also be used in teaching logic and theorem proving.