All entries for November 2005

Design Phase

Java Chosen
Java has been chosen as the language in which the tool will be implemented primarily for the following reasons:

• The author has more experience with Java;
• Java is native OOP, therefore more natural for implemenenting data structures;
• Java is almost as portable as a web based solution and faster.

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:

• They should be simple for a user to describe;
• They should be simple for the program to interpret and use.

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 p_n is a propositional atom:

p₁ AND p₂ GIVES p₁

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:

1. The rules are encoded in such a general way that they can simply be read in from a file and slot straight into the program;
2. The rules are complied into Java code at runtime and form a seperate class.

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 p₁ \/ p₂ and then selects the \/-elimination rule, two boxes will open, one on top of each other; one for p₁ and another for p₂.

: 17 Nov 2005 01:44 |  Comments (0) |  Close comments |  Report a problem