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.

• Some logical issues in discrete mathematics and algorithmic thinking

  243-258

  Viviane Durand-Guerrier

  Views:

  98

  The role of logic in mathematics education has been widely discussed from the seventies and eighties during the “modern maths period” till now, and remains still a rather controversial issue in the international community. Nevertheless, the relevance of discrete mathematics and algorithmic thinking for the development of heuristic and logical competences is both one of the main points of the program of Tamás Varga, and of some didactic teams in France. In this paper, we first present the semantic perspective in mathematics education and the role of logic in the Hungarian tradition. Then, we present insights on the role of research problems in the French tradition. Finely, we raise some didactical issues in algorithmic thinking at the interface of mathematics and computer science.

  Subject Classification: 97E30

• Difference lists in Prolog

  73-87

  Attila Csenki

  Views:

  26

  Prolog is taught at Bradford University within the two-semester module Symbolic and Declarative Computing/Artificial Intelligence. Second year undergraduate students are taught here the basics of the functional and the logic programming paradigms, the latter by using the Linux implementation of SWI Prolog [6]. The topic 'Difference lists' is mentioned in traditional textbooks such as [2] and [5] but it was felt that the available texts do not quite serve our purposes. We present here a lecture handout and a laboratory sheet for the teaching sessions on Difference lists. It is believed that the lectures and lab sessions together with the handouts shown here are a gentle, self-contained and reasoned introduction into the topic. The figures here shown to illustrate the concepts are considered a special feature of the handouts which in this form do not seem to be well known.

• An e-learning environment for elementary analysis: combining computer algebra, graphics and automated reasoning

  13-34

  Róbert Vajda

  Views:

  34

  CreaComp is a project at the University of Linz, which aims at producing computer-supported interactive learning units for several mathematical topics at introductory university level. The units are available as Mathematica notebooks. For student experimentation we provide computational, graphical and reasoning tools as well. This paper focuses on the elementary analysis units.
  The computational and graphical tools of the CreaComp learning environment facilitate the exploration of new mathematical objects and their properties (e.g., boundedness, continuity, limits of real valued functions). Using the provided tools students should be able to collect empirical data systematically and come up with conjectures. A CreaComp component allows the formulation of precise conjectures and the investigatation of their validity. The Theorema system, which has been integrated into the CreaComp learning environment, provides full predicate logic with a user-friendly twodimensional syntax and a couple of automated reasoners that produce proofs in an easy-to-read and natural presentation. We demonstrate the learning situations and the provided tools through several examples.