Writing about web page http://www.dcs.warwick.ac.uk/~csucix/index.html
This is a screen shot of PLoTT in its latest incarnation. Hopefully this may enourage some more people to download it and let me know how they get on! Download PLoTT here!
19 Apr 2006 15:27
| 
Comments (2)
| 
Report a problem
Writing about web page http://www.dcs.warwick.ac.uk/~csucix/download.html
I've had some feedback from Lee Herrington (thanks Lee!). It seems that PLoTT v0.1 didn't do enough validation on user entered formulae and as a result would output horrible Java errors to the command line. After having a brain wave on how to check that user entered formulae are well-formed, I implemented the code and have uploaded the changes.
18 Apr 2006 15:34
| Comments (0)
| Report a problem
Writing about web page http://www.dcs.warwick.ac.uk/~csucix/
You can now download PLoTT ("Propositional Logic Teaching Tool") from its website .
Any thoughts, comments or suggestions are welcome. In terms of future development, I intend to release the source code under the GPL should anyone wish to carry on with it. Please, if you have a spare five minutes and are interested in / have studied natural deduction, please give it a whirl and send me some feedback! Deadline for my report is 20th April, so anything you send could feature :)
17 Apr 2006 20:48
| Comments (1)
| Report a problem
Just a note-to-self to say that the rules.java file produced by JavaCC needs to be compiled using:
javac -source 1.4 rules.java
Otherwise it breaks. Horribly.
28 Feb 2006 11:07
| Comments (0)
| Report a problem
Summary
Development phase is nearing completion. The authors hopes to have the first version ready by Monday, ready for testing with undergraduates. Again, if anyone is interested in testing this tool please e-mail the author (use the contact form above).
User Interface and Swing
The author has learnt Swing concurrently with developing the interface. There was a reasonably steep learning curve to overcome as a WYSIWYG IDE wasn't used to implement the GUI. Instead, the author has used Eclipse which is a fantastic IDE for Java.
Note that the toolbar and the (blank) menu bar have yet to be implemented. The bottom right hand area of whitespace is reserved for some shortcut buttons and a preview window of the rule selected in the top right.
Back End
The backend is all but complete; small bugs are being ironed out as the GUI is developed. This is because the GUI is being built to fit around the "back office" aspect of the project. Inspired by the MVC model, the back end will be almost entirely seperate from the front end in the sense that someone wishing to re-write the GUI will theoretically be able to.
Rule Compiler
The rule compiler is fully implemented in JavaCC and is ready to be included in the final release of the project, save for documentation (see below).
Documentation
Documentation has yet to begin. Code is commented in such a way that the author can document the code at a later stage. It is expected that a full JavaDoc of the project will be available should anyone wish to develop or extend the project.
Methodology
Following design work over Christmas, the development has been conducted in a code-and-test manner, similar to the XP methodology.
23 Feb 2006 01:20
| Comments (3)
| Report a problem
Java Chosen
Java has been chosen as the language in which the tool will be implemented primarily for the following reasons:
Rules: Encoding and Implementing
Deciding on how to encode the rules and then how to incorporate them into the program is complex. The requirements for the rules are thus:
Initially, these two objectives are apparently mutually exclusive. The first is relativley straight forward, near-natural language would be enough. For instance, take the /\-elimination-1 rule. It could be described in the following manner, where pn is a propositional atom:
p1 AND p2 GIVES p1
However, getting Java to interpret this into something meaningful to it will be harder. An other (absurd) option would be to make the user, given a strict set of guidelines, write the rule out in Java. Instead, the former or an implementation similar to the former is the more viable option. The problem is how to convert this into Java code. There are two options:
If the user is to be given any degree of flexibility, the first option seems highly unlikely. The second, however, seems to hold more potential. If a grammar can be formed to suitably describe any propositional logic rule, a compiler could be designed and included with the tool to take the written rules, parse them and compile them into a class that could load upon run time.
Preliminary investigations suggest that implementing a grammar to represent a rule would not be overly complex. Below is the first few lines of what such a grammar may look like in Bachus-Naur Form (BNF).
Once a grammar has been defined, a tool such as JavaCC can be used to create a program that takes a file as input and produces Java code as output. Once compiled, this code will form the rules section of the program.
Data Structures
As discussed in a previous entry, trees seem to be the most natural way of representing a formula within the program. To store multiple formula and to introduce a notion of scope, the following diagram illustrates how linked lists could be used.
Note that individual formulas here are represented in postfix notation; achieved by doing a post-order traversal on a tree such as the one given below. The red lines indicate a linked list where a box has been opened in the proof. The green lines are pointers from each element of the list to an item in the GUI. Elements of a linked list can only interact with elements from the same linked list of from elements from a linked list above. This introduces the required notion of scope. As an element is deleted from a linked list, the pointer from the GUI to the element remains and indeed can be reconnected if an error has been made.
\/-elimination Rule
This rule is one of the more complex to implement, so some thought has been dedicated to how it and others like it will be implemented. The proposed solution is thus. When a user selects a line of the form p1 \/ p2 and then selects the \/-elimination rule, two boxes will open, one on top of each other; one for p1 and another for p2.
17 Nov 2005 01:44
| Comments (0)
| Report a problem
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)
| Report a problem
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)
| Report a problem
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)
| Report a problem
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)
| Report a problem
Loading…
Please wait - comments are loading