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) |  Report a problem