All entries for October 2005

Tree / Graph Drawing Tools

Is anyone aware of a tool that can be used for the drawing of graphs / tools, such as the one in this entry? Such a tool would almost certainly be useful for this project.

If you are aware of such a tool, please do let me know.

: 26 Oct 2005 11:40 |  Comments (5) |  Close comments |  Report a problem

Revised Timetable

Follow-up to Thinking about Implementation from Logic Teaching Tool

From the project specification:

Detailed feature list following research into existing theorem proving / proof editing tools. For review.

These past two weeks have been spent considering the implementation. Following some initial research into other proof editors and theorem solvers, it became apparent that the exercise was fruitless, purely because the aims of the project are clear enough to make other (similar) implementations irrelevant. Perhaps in the construction of the writeup, a small section on other tools will be included.

: 25 Oct 2005 23:16 |  Comments (0) |  Close comments |  Report a problem

Thinking about Implementation

Introduction
The following notes are some of the options and challenges that will be examined whilst designing and implementing both the GUI and the datastructure aspects of the project.

Java vs Perl & HTML
Although the specification lists Java as the intended language to use for implementation, a web-based implementation based upon Perl and HTML is now being considered. Using HTML over Java for the user interface has advantages, mainly because the user is more familiar with HTML than any Java GUIs. Specifically, tables in HTML and the border property seem a natural way of representing proof boxes. Choosing HTML for the GUI would require some (or lots of!) Perl to be running server side as HTTP is inherently stateless, this is a potential problem as the GUI may suffer in terms of ease of use.

In the defence of Java, the author's trepidation comes from ignorance of designing GUI interfaces in Java. Furthermore, creating the data structures required in Java will be easier, if only if it is because it is the author's 'primary' language. Some research into the area of GUI design with Java is necessary before deciding firmly on the language(s) to be used for implementation.

Data Structures
Displaying the propositional atoms, assumptions and so on is one thing, yet representing them internal to the program is another. The most natural way of storing a propositional logic formulae is by using a tree (see right). How does this translate into representing a proof? The reader will be familiar with the structure of a propositonal proof; firstly a set of premises are noted or an assumption is made and via a set of proof rules a conclusion is reached. This presents a problem that will be one of the main challenges of the implementation.

Boxes can be nested and new ones can be open after old ones are closed. One a box is closed, only the resulting formula can be subsequently used; that's to say boxes have scope much in the same way that variables have scope within a program. How is it possible to program a proof editior whilst being mindful of this nature of scope?

For a moment, let us pretend that there are no assumptions (or boxes, the words are often, but not always, interchangable) in a given proof. There will be no issues with scope, as from premise to conclusion everything will be in scope. A convienient way to represent each line of the proof would be it's own individual proof tree, so the whole proof could be represented as, say, a linked list of proof trees.

Introducing an assumption into this proof presents the afforementioned problems associated with scope. Clearly, some notion of heirachy is present in the concept of scope. The main challenge for consideration here is to preserve this notion, whilst retaining the details of the proof from within the box. Something to think about.

: 25 Oct 2005 22:40 |  Comments (0) |  Close comments |  Report a problem

Specification Decisions

This entry follows a meeting with Dr. Lazic and discusses some of the final decisions made for the specification of the project.

Propositional Logic Only
Implementing some aspects of predicate logic, such as the binding properties of the quantifiers, may make it hard to complete the project. Instead, this is now an additional aim rather than a core one.

Non-hardcoded Rules
For flexibility, the rules (e.g. /\-introduction, \/-elimination) will be defined in a text file, not hardcoded. This will allow a user to expand or reduce the rules they can use as they see fit. For example, implication can be formed from 'and' and 'or', so reducing the set of rules to such that only 'and' and 'or' rules are available will make proofs more challenging.

Open / Close Box Structure
Some proof editors use a tree to display the proof that the user is working on. This project will implement the open / close box structure familiar in both the lectures for CS205 and the Huth & Ryan. It is hoped that this visual similarity will contribute to the aim below.

Ease of Use and Educational
To reiterate, the aim of this project is to be educational. Therefore, the tool must be intuitive to use if it is to help the user learn and develop their skill with propositional logic.

: 12 Oct 2005 11:39 |  Comments (0) |  Close comments |  Report a problem

Introduction

This blog will be used to maintain a record of the progress of the author's third year project. The project is the design and implementation of a logic tutor, primarily with the Computer Science module CS205: Logic For Computer Scientists in mind.

The project supervisor for this module is Dr. Ranko Lazic who is the current lecturer for Logic.

If you have any questions about the project or would like to volunteer to test it, please use the contact link above.

Why 'Logic Teaching Tool' as a title?

The alternative question is 'why not a logic proof editor or a theorem prover'. Writing a proof editor on it's own would be duplicating the work of others such as the aptly named Just Another Theorem Prover (aka JAPE) written by the comlab at Oxford, so duplicating the existing work of academics seems pointless and unrewarding. Secondly, there is little scope for improvement on existing theroem provers. Therefore, the aim of this project is to produce a useful and useable teaching tool aimed at undergraduate students who are starting out in studying this core computer science topic studied in most computer science courses.

Why a teaching tool in the first place?

Studying the proof aspect of Logic For Computer Scientists has a steep learning curve. Knowing which rules to use and when to use them is often confusing. At first, making seemingly baseless or random assumptions to draw conclusions from is counter-intuitive. By providing an intelligent tool that a user can perform proofs with will reduce the learning curve whilst encouraging exploratory learning. An additional aim is to graphically replicate the box like proof structure familiar to students.

How will the success of the project be measured?

This tool is intended to be used as a teaching aid. Therefore it seems logical (please excuse the pun) that it is tested and evaluated by current second year students who have studied CS205. If you are interested in volunteering to test this project towards the end of term 2, please contact the author using the contact link above.

: 05 Oct 2005 14:37 |  Comments (0) |  Close comments |  Report a problem