All entries for Tuesday 25 October 2005

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