### 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.

## No comments

## Add a comment

You are not allowed to comment on this entry as it has restricted commenting permissions.