October 12, 2005

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 Not publicly viewable

Add a comment

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

October 2005

Mo Tu We Th Fr Sa Su
|  Today  | Nov
               1 2
3 4 5 6 7 8 9
10 11 12 13 14 15 16
17 18 19 20 21 22 23
24 25 26 27 28 29 30

Search this blog


Most recent comments

  • Thanks Darren, very very useful! by Anum on this entry
  • what is this site on haha by sam on this entry
  • omg by curtis on this entry
  • I have e–mailed this response to William: This is a "feature"; due to the way assumption boxes have … by on this entry
  • This is a great little program, but the line numbers don't line up for me. I'm using blackbox 0.7 as… by William Starling on this entry

Blog archive

Not signed in
Sign in

Powered by BlogBuilder