Search

Search Results

• Linear clause generation by Tableaux and DAGs

  109-118

  Gergely Kovásznai

  Views:

  32

  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.

• Heuristic arguments and rigorous proofs in secondary school education

  167-184

  Zsolt Fülöp

  Views:

  32

  In this paper we are going to discuss some possible applications of the mechanical method, especially the lever principle, in order to formulate heuristic conjectures related to the volume of three-dimensional solids. In the secondary school educational processes the heuristic arguments are no less important than the rigorous mathematical proofs. Between the ancient Greek mathematicians Archimedes was the first who made heuristic conjectures with the methods of Mechanics and proved them with the rigorous rules of Mathematics, in a period, when the methods of integration were not known. For a present day mathematician (or a secondary school mathematics teacher) the tools of the definite integral calculus are available in order to calculate the volume of three dimensional bodies, such as paraboloids, ellipsoids, segments of a sphere or segments of an ellipsoid. But in the secondary school educational process, it is also interesting to make heuristic conjectures by the use of the Archimedean method. It can be understood easily, but it is beyond the normal secondary school curriculum, so we recommend it only to the most talented students or to the secondary schools with advanced mathematical teaching programme.

• Analysis of a problem in plane geometry discussed in an 11th grade group study session

  181-193

  Richárd Rakamazi

  Views:

  27

  The main aim of this paper is to show those strategies and proof methods we try to teach in secondary maths education through an interesting geometric problem: Find a relation for the sides of a triangle where an angle is the double of another angle. Is the converse also true? Is it possible to generalize the problem? We try to answer these questions while discussing the upcoming difficulties in detail and presenting more possible solutions. Hopefully the paper can be successfully used in study group sessions and problem solving seminars in secondary schools.

• The shift of contents in prototypical tasks used in education reforms

  203-219

  Karl Joseph Fuchs

  Views:

  93

  The paper discusses the shift of contents in prototypical tasks provoked by the current educational reform in Austria. The paper starts with the educational backboard of the process of changes in particular with the out tting of the students' abilities in different taxonomies and its implementation in the competence models of Mathematics. A methodological didactical point of view on the process is given additionally. Examples out of a specific collection of math problems which arise from the educational reform are integrated and analysed in the context of educational principles and methods. The discussion ends with a short evaluation of the role of traditional approaches to tasks in the ongoing reform. A bundle of tasks as proof that they are still alive is presented finally.

  Subject Classification: 97B50, 97D40, 97D50